论文部分内容阅读
为保证SCADE软件开发的安全性，研究了SCADE形式化验证技术，指出其不足，提出了基于代码生成器的解决方法。该方法对安全特性属性引入了逻辑描述，并利用SCADE编辑器及代码生成器的特点，对SCADE形式化验证技术进行改进，降低了模型正确性确认时人为的主观性。通过实例阐述了应用该方法进行形式化验证的一般步骤，表明了该方法是有效可行的。