Rigorous development process of a safety-critical system: from ASM models to Java code
Rigorous development process of a safety-critical system: from ASM models to Java code
复制标题
安全关键系统的严格开发流程：从 ASM 模型到 Java 代码
DOI：
10.1007/s10009-015-0394-x
复制
发表时间：
2015
影响因子：
1.5
通讯作者：
E. Riccobene
中科院分区：
文献类型：
--
作者：
Paolo Arcaini;A. Gargantini;E. Riccobene
提出了一种基于抽象状态机形式化方法的安全关键系统严格开发方法。开发过程从系统的高级正式视图开始，通过细化，导出更详细的模型，直到所需的规范级别。沿着该过程，可以进行不同的确认和验证活动，如模拟、模型审查和模型检查。此外，可以使用基于SMT的方法证明每个细化步骤是正确的。作为细化过程的最后一步，可以开发Java实现并将其链接到正式规范。实现的正确性w.r.t.通过基于模型的测试和运行时验证，可以证明其形式化规格说明。最后以某起落架系统为例进行了仿真分析。
The paper presents an approach for rigorous development of safety-critical systems based on the Abstract State Machine formal method. The development process starts from a high level formal view of the system and, through refinement, derives more detailed models till the desired level of specification. Along the process, different validation and verification activities are available, as simulation, model review, and model checking. Moreover, each refinement step can be proved correct using an SMT-based approach. As last step of the refinement process, a Java implementation can be developed and linked to the formal specification. The correctness of the implementation w.r.t. its formal specification can be proved by means of model-based testing and runtime verification. The process is exemplified by using a Landing Gear System as case study.