计算机工程
計算機工程
계산궤공정
COMPUTER ENGINEERING
2014年
8期
302-309
,共8页
非严格实时系统%形式化规格说明%责任策略%分布式时态逻辑%Object-Z语言%历史不变式
非嚴格實時繫統%形式化規格說明%責任策略%分佈式時態邏輯%Object-Z語言%歷史不變式
비엄격실시계통%형식화규격설명%책임책략%분포식시태라집%Object-Z어언%역사불변식
soft real-time system%formal specification%obligation policy%distributed temporal logic%Object-Z language%history invariant
严格实时系统行为的实时性要求具有不可更改性,非严格实时系统的实时性要求则具有延缓性、替代性以及可补偿性特征,现有的形式化规格说明语言多集中在对严格实时系统的研究,对非严格实时系统的这些特征则缺乏描述能力.针对上述问题,使用一种Object-Z扩展语言来描述非严格实时系统,该方法采用扩展的Object-Z历史不变式表达责任策略,能有效地描述非严格实时系统中的缺省策略、补偿策略以及其他非严格实时策略.以会议系统为例,说明该方法能形式化描述非严格实时行为,具有较强的实用性.
嚴格實時繫統行為的實時性要求具有不可更改性,非嚴格實時繫統的實時性要求則具有延緩性、替代性以及可補償性特徵,現有的形式化規格說明語言多集中在對嚴格實時繫統的研究,對非嚴格實時繫統的這些特徵則缺乏描述能力.針對上述問題,使用一種Object-Z擴展語言來描述非嚴格實時繫統,該方法採用擴展的Object-Z歷史不變式錶達責任策略,能有效地描述非嚴格實時繫統中的缺省策略、補償策略以及其他非嚴格實時策略.以會議繫統為例,說明該方法能形式化描述非嚴格實時行為,具有較彊的實用性.
엄격실시계통행위적실시성요구구유불가경개성,비엄격실시계통적실시성요구칙구유연완성、체대성이급가보상성특정,현유적형식화규격설명어언다집중재대엄격실시계통적연구,대비엄격실시계통적저사특정칙결핍묘술능력.침대상술문제,사용일충Object-Z확전어언래묘술비엄격실시계통,해방법채용확전적Object-Z역사불변식표체책임책략,능유효지묘술비엄격실시계통중적결성책략、보상책략이급기타비엄격실시책략.이회의계통위례,설명해방법능형식화묘술비엄격실시행위,구유교강적실용성.
