微电子学与计算机
微電子學與計算機
미전자학여계산궤
MICROELECTRONICS & COMPUTER
2006年
2期
16-19
,共4页
肖健宇%张德运%陈海诠%董皓
肖健宇%張德運%陳海詮%董皓
초건우%장덕운%진해전%동호
时态规约%形式化方法%实时系统%B方法%B函数
時態規約%形式化方法%實時繫統%B方法%B函數
시태규약%형식화방법%실시계통%B방법%B함수
提出一套利用B方法中经典AMN记号表达时态规约的函数结构方案以支持实时软件系统的规约和验证.该方案中,时间类型表示为B方法中系统内部支持的非负整数集合,所有依赖于时间的变量都表示成定义域为时间的全函数.该方案可以方便地表达"过去"、"现在"、"稳定"、"跳变"等时态概念.定义了时间类型、"现在"以及与时间有关的变量的宏操作等抽象机,这些抽象机已经通过B工具的一致性验证,可以在实时系统的B形式化规约中直接使用.
提齣一套利用B方法中經典AMN記號錶達時態規約的函數結構方案以支持實時軟件繫統的規約和驗證.該方案中,時間類型錶示為B方法中繫統內部支持的非負整數集閤,所有依賴于時間的變量都錶示成定義域為時間的全函數.該方案可以方便地錶達"過去"、"現在"、"穩定"、"跳變"等時態概唸.定義瞭時間類型、"現在"以及與時間有關的變量的宏操作等抽象機,這些抽象機已經通過B工具的一緻性驗證,可以在實時繫統的B形式化規約中直接使用.
제출일투이용B방법중경전AMN기호표체시태규약적함수결구방안이지지실시연건계통적규약화험증.해방안중,시간류형표시위B방법중계통내부지지적비부정수집합,소유의뢰우시간적변량도표시성정의역위시간적전함수.해방안가이방편지표체"과거"、"현재"、"은정"、"도변"등시태개념.정의료시간류형、"현재"이급여시간유관적변량적굉조작등추상궤,저사추상궤이경통과B공구적일치성험증,가이재실시계통적B형식화규약중직접사용.
