Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems

Meseguer, José; Olveczky, Peter C.

Permalink

https://hdl.handle.net/2142/17089 Copy

Description

Title

Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems

Author(s)

• Meseguer, José
• Olveczky, Peter C.

Issue Date

2010-09-13

Keyword(s)

real-time distributed systems, software patterns, formal verification, model checking

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 communicating asynchronously among themselves and with their environment 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 DTRS. This work presents a formal specification of PALS as a formal model transformation that maps a synchronous design, together with a set of 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 is used to illustrate the usefulness of PALS for formal verification purposes.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/17089

Owning Collections