摘要
首先将软件的UML状态机模型转换为模型检测工具MOCHA的输入语言REACTIVEMODULES,在MOCHA中进行正确性验证,利用模型检测工具针对错误情况给出的反例路径,尽早修改软件的UML设计模型;然后将已验证过的UML模型转换为定理证明工具B方法的抽象规约,利用B方法的精化、验证及代码生成功能,直接生成正确的C代码。并给出了从UML状态机到REACTIVE MODULES建模语言及B AMN抽象规约的转换规则。实验结果表明,该方法可在软件工程中有效地提高高可信嵌入式软件开发和验证的效率。
UML state machine model of software was transformed into the input language of model checker MOCHA and was checked in it. The model checker gave counterexamples path according to the flaw found in the model checked, which could modify the software UML design model. The verified UML model was transformed into abstract specifications of B method, in which it can be refined, verified and translated into source C code. The rules of transformation from UML state machine to REACTIVE MODULES modelling language and B AMN abstract specifications were put forward. The experimental result shows that the strategy could significantly improves the efficiency of development and verification of high-confidence embedded software.
出处
《吉林大学学报（工学版）》
EI
CAS
CSCD
北大核心
2005年第5期531-536,共6页
Journal of Jilin University:Engineering and Technology Edition
基金
"863"国家高技术研究发展计划基金资助项目(863-301-05-03).
