基于SCADE的形式化验证技术的改进研究  

Research on improvement of SCADE-based formal verification technology

作　　者：李耀[1] 郭进[1] 孔令晶[1] 宋海权[1] 

机构地区：[1]西南交通大学信息科学与技术学院,四川成都610031

出　　处：《计算机工程与设计》2013年第6期2025-2030,共6页Computer Engineering and Design

基　　金：铁道部科技研究开发计划基金项目(2012X007-D)

摘　　要：为保证SCADE软件开发的安全性,研究了SCADE形式化验证技术,指出其不足,提出了基于代码生成器的解决方法。该方法对安全特性属性引入了逻辑描述,并利用SCADE编辑器及代码生成器的特点,对SCADE形式化验证技术进行改进,降低了模型正确性确认时人为的主观性。通过实例阐述了应用该方法进行形式化验证的一般步骤,表明了该方法是有效可行的。To ensure the safety of SCADE-Based software development, SCADE-Based formal verification technology is studied. Through analyzing the limitations, a novel solution based on code generator is presented. A logic description way is introduced for safety property and the feature of SCADE editor and code generator is utilized, SCADE-based formal verification is improved so that reduces the subjectivity of the model＇s validation. The general steps of the method application are elaborated by an example, which indicates the solution is effective.

关 键 词：高安全性应用开发环境 形式化验证 安全特性观察器 逻辑描述 模型安全 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]