微电子学与计算机
微電子學與計算機
미전자학여계산궤
MICROELECTRONICS & COMPUTER
2005年
8期
80-84
,共5页
肖健宇%张德运%董皓%陈海诠
肖健宇%張德運%董皓%陳海詮
초건우%장덕운%동호%진해전
UML状态机%形式化方法%B方法%高可信软件工程
UML狀態機%形式化方法%B方法%高可信軟件工程
UML상태궤%형식화방법%B방법%고가신연건공정
文章研究在高可信软件工程中集成形式化方法.以软件设计的UML状态机模型为起点,将其转换为B形式化模型,然后在B工具环境中遵循B方法的精化原则和正确性验证方法,开发出可靠的实现模型.提出一套从UML状态机到B形式化规约的转换规则,涵盖UML基本状态图、分层状态图和并发状态图.实例分析表明,这套转换规则行之有效.
文章研究在高可信軟件工程中集成形式化方法.以軟件設計的UML狀態機模型為起點,將其轉換為B形式化模型,然後在B工具環境中遵循B方法的精化原則和正確性驗證方法,開髮齣可靠的實現模型.提齣一套從UML狀態機到B形式化規約的轉換規則,涵蓋UML基本狀態圖、分層狀態圖和併髮狀態圖.實例分析錶明,這套轉換規則行之有效.
문장연구재고가신연건공정중집성형식화방법.이연건설계적UML상태궤모형위기점,장기전환위B형식화모형,연후재B공구배경중준순B방법적정화원칙화정학성험증방법,개발출가고적실현모형.제출일투종UML상태궤도B형식화규약적전환규칙,함개UML기본상태도、분층상태도화병발상태도.실례분석표명,저투전환규칙행지유효.
