TY - GEN
T1 - Formalization and correctness of the pals architectural pattern for distributed real-time systems
AU - Meseguer, José
AU - Ölveczky, Peter Csaba
N1 - Funding Information:
This work is part of a broader collaboration with Steve Miller and Darren Cofer at Rockwell-Collins and with Lui Sha, Abdullah Al-Nayeem, and Mu Sun at UIUC on the PALS architecture. The PALS ideas have been developed in close interaction with all these people, who have provided very useful comments on earlier versions of this work. We thank in particular Lui Sha and Mu Sun, as well as the anonymous reviewers, for their very careful and insightful comments on earlier versions of this paper that have led to substantial improvements, and Abdullah Al-Nayeem for providing us with an AADL model of an avionics system that we have used as our basis in Section 9. We also thank Camilo Rocha for his kind help with some of the figures. We gratefully acknowledge funding for this research from the Rockwell-Collins Corporation. Partial support has also been provided by the National Science Foundation under Grants IIS 07-20482, CNS 08-34709, and CCF 09-05584, by the Boeing Corporation under Grant C8088-557395, and by the Research Council of Norway through the Rhytm project.
PY - 2010
Y1 - 2010
N2 - Many Distributed Real-Time Systems (DRTS), such as integrated modular avionics systems and distributed control systems in motor vehicles, are made up of a collection of components that communicate asynchronously and that must change their state and respond to environment inputs within hard real-time bounds. Such systems are often safety-critical and need to be certified; but their certification is currently very hard due to their distributed nature. The Physically Asynchronous Logically Synchronous (PALS) architectural pattern can greatly reduce the design and verification complexities of achieving virtual synchrony in a DRTS. This work presents a formal specification of PALS as a formal model transformation that maps a synchronous design, together with performance bounds of the underlying infrastructure, to a formal DRTS specification that is semantically equivalent to the synchronous design. This semantic equivalence is proved, showing that the formal verification of temporal logic properties of the DRTS can be reduced to their verification on the much simpler synchronous design. An avionics system case study illustrates the usefulness of PALS for formal verification purposes.
AB - Many Distributed Real-Time Systems (DRTS), such as integrated modular avionics systems and distributed control systems in motor vehicles, are made up of a collection of components that communicate asynchronously and that must change their state and respond to environment inputs within hard real-time bounds. Such systems are often safety-critical and need to be certified; but their certification is currently very hard due to their distributed nature. The Physically Asynchronous Logically Synchronous (PALS) architectural pattern can greatly reduce the design and verification complexities of achieving virtual synchrony in a DRTS. This work presents a formal specification of PALS as a formal model transformation that maps a synchronous design, together with performance bounds of the underlying infrastructure, to a formal DRTS specification that is semantically equivalent to the synchronous design. This semantic equivalence is proved, showing that the formal verification of temporal logic properties of the DRTS can be reduced to their verification on the much simpler synchronous design. An avionics system case study illustrates the usefulness of PALS for formal verification purposes.
UR - http://www.scopus.com/inward/record.url?scp=78649543257&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78649543257&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-16901-4_21
DO - 10.1007/978-3-642-16901-4_21
M3 - Conference contribution
AN - SCOPUS:78649543257
SN - 3642169007
SN - 9783642169007
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 303
EP - 320
BT - Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings
T2 - 12th International Conference on Formal Engineering Methods, ICFEM 2010
Y2 - 17 November 2010 through 19 November 2010
ER -