计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2006年
8期
64-66
,共3页
肖健宇%张德运%陈海诠%董皓
肖健宇%張德運%陳海詮%董皓
초건우%장덕운%진해전%동호
B方法%形式化方法%UML状态机%嵌入式软件%高可信软件工程
B方法%形式化方法%UML狀態機%嵌入式軟件%高可信軟件工程
B방법%형식화방법%UML상태궤%감입식연건%고가신연건공정
提出了一套集成UML与B方法开发高可信嵌入式软件的实用方案:以软件的UML状态机模型为起点,将其转换为B抽象模型并在B工具中验证该模型的一致性,然后遵循B模型逐步精化的开发规则,利用B方法的精化正确性验证功能,得到系统的可靠的实现模型,最后借助B工具自动生成C代码.实例分析表明,这套方法可以提高高可信嵌入式软件的开发验证效率.给出了嵌入式软件设计中常用的UML并发状态图到B抽象模型的转换规则.
提齣瞭一套集成UML與B方法開髮高可信嵌入式軟件的實用方案:以軟件的UML狀態機模型為起點,將其轉換為B抽象模型併在B工具中驗證該模型的一緻性,然後遵循B模型逐步精化的開髮規則,利用B方法的精化正確性驗證功能,得到繫統的可靠的實現模型,最後藉助B工具自動生成C代碼.實例分析錶明,這套方法可以提高高可信嵌入式軟件的開髮驗證效率.給齣瞭嵌入式軟件設計中常用的UML併髮狀態圖到B抽象模型的轉換規則.
제출료일투집성UML여B방법개발고가신감입식연건적실용방안:이연건적UML상태궤모형위기점,장기전환위B추상모형병재B공구중험증해모형적일치성,연후준순B모형축보정화적개발규칙,이용B방법적정화정학성험증공능,득도계통적가고적실현모형,최후차조B공구자동생성C대마.실례분석표명,저투방법가이제고고가신감입식연건적개발험증효솔.급출료감입식연건설계중상용적UML병발상태도도B추상모형적전환규칙.
