Introduction
Distributed real-time systems (DRTSs), such as avionics and automotive systems, are very hard to design and verify. Besides the dif- ficulties of asynchrony, clock skews, and network delays, an additional source of complexity comes from the multirate nature of many such sys- tems, which must implement several levels of hierarchical control at dif- ferent rates. In this work we present several simple model transformations and a multirate extension of the PALS pattern which can be combined to reduce the design and verification of a virtually synchronous multi- rate DRTS to the much simpler task of specifying and verifying a single synchronous system.
The Maude Framework for Modeling Multi-rate PALS
We define an executable formal semantic framework for the multi-rate ensemble patterns that can be used for simulation and formal verification.
This Maude specification can be instantiated to any multirate ensemble of interest and is very useful for formal analysis purposes, since it will have much fewer states than, yet will be bisimilar to the corresponding asynchronous model.
In addition to the
Maude system, this framework also requires the
Full Maude for object-oriented style semantics.
- multirate-ensemble.maude: the Maude semantics for the multi-rate Pals.
- airplane.maude: the example using the multi-rate PALS Maude framework, including the specification of the airplane control system system and the verification of a simple safety property.
You can also find the updated version of the Real-Time Maude semantics and the case study here.
The Airplane Turning System by Josh Krisiloff
Our example is inspired by Josh Krisiloff's class project for the
program varification class in UIUC. He specified a simple airplane turning control system in the
Real-Time Maude, and performed simulations with some initial parameters. See his report for more details.