首页> 外文期刊>Computer Languages, Systems & Structures >Compiling and verifying SC-SystemJ programs for safety-critical reactive systems
【24h】

Compiling and verifying SC-SystemJ programs for safety-critical reactive systems

机译:编译和验证安全关键型反应系统的SC-SystemJ程序

获取原文
获取原文并翻译 | 示例

摘要

Most of today's embedded systems are very complex. These systems, controlled by computer programs, continuously interact with their physical environments through network of sensory input and output devices. Consequently, the operations of such embedded systems are highly reactive and concurrent. Since embedded systems are deployed in many safety-critical applications, where failures can lead to catastrophic events, an approach that combines mathematical logic and formal verification is employed in order to ensure correct behavior of the control algorithm. This paper presents What You Prove Is What You Execute (WYPIWYE) compilation strategy for a Globally Asynchronous Locally Synchronous (GALS) programming language called Safey-Critical SystemJ. SC-SysternJ is a safety-critical subset of the SystemJ language. A formal big-step transition semantics of SC-SystemJ is developed for compiling SC-SystemJ programs into propositional Linear Temporal Logic formulas. These LTL formulas are then converted into a network of Mealy automata using a novel and efficient compilation algorithm. The resultant Mealy automata have a straightforward syntactic translation into Promela code. The resultant Promela models can be used for verifying correctness properties via the SPIN model-checker. Finally there is a single translation procedure to compile both: Promela and C/Java code for execution, which satisfies the De-Bruijn index, i.e. this final translation step is simple enough that is can be manually verified. (C) 2015 Elsevier Ltd. All rights reserved.
机译:当今大多数嵌入式系统都非常复杂。这些由计算机程序控制的系统通过感官输入和输出设备的网络不断与其物理环境进行交互。因此,这种嵌入式系统的操作是高度反应性的和并行的。由于嵌入式系统已部署在许多安全关键型应用程序中,在这些应用程序中,故障可能导致灾难性事件,因此采用了一种将数学逻辑和形式验证相结合的方法,以确保控制算法的正确行为。本文介绍了一种称为“安全关键系统J”的全局异步本地同步(GALS)编程语言的“证明就是执行”(WYPIWYE)编译策略。 SC-SysternJ是SystemJ语言的安全关键子集。开发了SC-SystemJ的形式化大步过渡语义,用于将SC-SystemJ程序编译为命题线性时间逻辑公式。然后,使用新颖高效的编译算法将这些LTL公式转换为Mealy自动机网络。生成的Mealy自动机具有直接转换为Promela代码的语法。生成的Promela模型可通过SPIN模型检查器用于验证正确性。最后,只有一个编译过程可以同时编译两者:Promela和C / Java代码以执行,该代码满足De-Bruijn索引,即,此最终翻译步骤非常简单,可以手动验证。 (C)2015 Elsevier Ltd.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号