Aiding Modular Design and Verification of Safety-Critical Time-Triggered Systems by Use of Executable Formal Specifications

摘要

Designing safety-critical systems is a complex process, and especially when the design is carried out at different levels of abstraction where the correctness of the design at one level is not automatically sustained over the next level. In this work we focus on time-triggered (TT) systems where the resources of communication and computation are shared among different applications to reduce the overall cost of the system. This entails serializing both communication and computation which does not necessarily meet the assumptions made by the application. Hence, we present the concept of executable formal specification of general TT systems to establish a faithful model of the TT characteristics. Our focus is on general applications running in a synchronous environment. The proposed model can be easily customized by the user and it is able to support simulation and verification of the system. It also aids the effective deployment of applications, and the validation of the real system with model-based test generation. Our case study shows how the general model can be implemented in the SAL language and how SAL's tool suite can be used to guidethe design of general TT systems.