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 veri???cation 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 de???ne 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 veri???cation effort, because it reduces the veri???cation 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 speci???cation language. Since such formal speci???cations are executable, they can be used as a basis for correct-by-construction code generation implementations of PALS.
展开▼
