Formalization and correctness of the pals architectural pattern for distributed real-time systems

José Meseguer, Peter Csaba Ölveczky

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings
Pages303-320
Number of pages18
DOIs
StatePublished - 2010
Event12th International Conference on Formal Engineering Methods, ICFEM 2010 - Shanghai, China
Duration: Nov 17 2010Nov 19 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6447 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Conference on Formal Engineering Methods, ICFEM 2010
Country/TerritoryChina
CityShanghai
Period11/17/1011/19/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Formalization and correctness of the pals architectural pattern for distributed real-time systems'. Together they form a unique fingerprint.

Cite this