A number of cyber-physical systems are hierarchical distributed control systems whose components operate with different rates, and that should behave in a virtually synchronous way. Designing such systems is hard due to asynchrony, skews of the local clocks, and network delays; furthermore, their model checking verification is typically unfeasible due to the state space explosion caused by the interleavings. The Multirate PALS formal pattern reduces the problem of designing and model checking such virtually synchronous multirate systems to the much simpler tasks of specifying and verifying their underlying synchronous design. To make the Multirate PALS design and verification methodology available within an industrial modeling environment, we define in this work the modeling language Multirate Synchronous AADL, which can be used to specify multirate synchronous designs using the AADL modeling standard. We then define the formal semantics of Multirate Synchronous AADL in Real-Time Maude, and integrate Real-Time Maude verification into the OSATE tool environment for AADL.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Jebali, Fatma; Lang, Frédéric; Mateescu, Radu: Formal modelling and verification of GALS systems using GRL and CADP (2016)
- Bae, Kyungmin; Ölveczky, Peter Csaba: Hybrid multirate PALS (2015)
- Bae, Kyungmin; Ölveczky, Peter Csaba; Meseguer, José: Definition, semantics, and analysis of multirate synchronous AADL (2014) ioport
- Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: Timed CTL model checking in Real-Time Maude (2012)