吉林大学学报（工学版）
吉林大學學報（工學版）
길림대학학보（공학판）
JOURNAL OF JILIN UNIVERSITY(ENGINEERING AND TECHNOLOGY EDITION)
2005年
5期
531-536
,共6页
肖健宇%张德运%陈海诠%董浩
肖健宇%張德運%陳海詮%董浩
초건우%장덕운%진해전%동호
计算机软件%模型检测%定理证明%高可信软件%软件正确性验证%MOCHA%B方法
計算機軟件%模型檢測%定理證明%高可信軟件%軟件正確性驗證%MOCHA%B方法
계산궤연건%모형검측%정리증명%고가신연건%연건정학성험증%MOCHA%B방법
首先将软件的UML状态机模型转换为模型检测工具MOCHA的输入语言REACTIVEMODULES,在MOCHA中进行正确性验证,利用模型检测工具针对错误情况给出的反例路径,尽早修改软件的UML设计模型;然后将已验证过的UML模型转换为定理证明工具B方法的抽象规约,利用B方法的精化、验证及代码生成功能,直接生成正确的C代码.并给出了从UML状态机到REACTIVE MODULES建模语言及B AMN抽象规约的转换规则.实验结果表明,该方法可在软件工程中有效地提高高可信嵌入式软件开发和验证的效率.
首先將軟件的UML狀態機模型轉換為模型檢測工具MOCHA的輸入語言REACTIVEMODULES,在MOCHA中進行正確性驗證,利用模型檢測工具針對錯誤情況給齣的反例路徑,儘早脩改軟件的UML設計模型;然後將已驗證過的UML模型轉換為定理證明工具B方法的抽象規約,利用B方法的精化、驗證及代碼生成功能,直接生成正確的C代碼.併給齣瞭從UML狀態機到REACTIVE MODULES建模語言及B AMN抽象規約的轉換規則.實驗結果錶明,該方法可在軟件工程中有效地提高高可信嵌入式軟件開髮和驗證的效率.
수선장연건적UML상태궤모형전환위모형검측공구MOCHA적수입어언REACTIVEMODULES,재MOCHA중진행정학성험증,이용모형검측공구침대착오정황급출적반례로경,진조수개연건적UML설계모형;연후장이험증과적UML모형전환위정리증명공구B방법적추상규약,이용B방법적정화、험증급대마생성공능,직접생성정학적C대마.병급출료종UML상태궤도REACTIVE MODULES건모어언급B AMN추상규약적전환규칙.실험결과표명,해방법가재연건공정중유효지제고고가신감입식연건개발화험증적효솔.
