Files in this item



application/pdfpals.pdf (360kB)
(no description provided)PDF


Title:Formalization and Correctness of the PALS Pattern for Asynchronous Real-Time Systems
Author(s):Jose Meseguer and Peter Olveczky
Subject(s):real-time systems, asynchrony, formal specification, rewriting logic, Real-Time Maude
Abstract:Due to physical requirements, what in essence and at a higher level of abstraction is a logically synchronous real-time system has to be often realized as a distributed, asynchronous system. Getting asynchronous real-time systems right is a very error prone and labor-intensive task. The Physically Asynchronous Logically Synchronous (PALS) architectural pattern can greatly reduce the design and verification complexities of achieving logical synchrony in a distributed real-time system implementation. The PALS philosophy is to provide a correct-by-construction pattern of very wide applicability. The main goal of this work is to make the PALS correctness property —applying to a wide range of designs— mathematically precise. For this, we define a formal model of the PALS transformation, and give formal requirements for the allowed logically synchronous system designs, and for the operating environments in which a resulting PALS distributed design is to be deployed. Based on such a formal model and formal requirements, we also give a mathematical proof of correctness for PALS, and a proof of optimality, showing that the PALS period is shortest possible. The PALS proof of correctness can greatly facilitate the formal verification effort, because it reduces the verification of a complex asynchronous real-time system to that of its much simpler synchronous high-level design. Our formal model is developed in rewriting logic using the Real-Time Maude specification language. Since such formal specifications are executable, they can be used as a basis for correct-by-construction code generation implementations of PALS.
Issue Date:2009-11-12
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Date Available in IDEALS:2009-11-12

This item appears in the following Collection(s)

Item Statistics