Aiding Modular Design and Verification of Safety-Critical Time-Triggered Systems by Use of Ezecutable 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 SALs tool suite can be used to guide the design of general TT systems.
Kohei Sakurai Peter Bokor Neeraj Suri
Hitachi Europe GmbH, Germany Technische Universitat Darmstadt, Germany
国际会议
11th IEEE High Assurance Systems Engineering Symposium(HASE 2008)(第十一届IEEE高可信系统工程国际研讨会)
南京
英文
261-270
2008-12-03（万方平台首次上网日期，不代表论文的发表时间）