基于责任策略的非严格实时系统形式化研究  

Formal Study of Soft Real-time System Based on Obligation Policy

作　　者：马莉[1] 钟勇[1] 霍颖瑜[1] 

机构地区：[1]佛山科学技术学院电子与信息工程学院,广东佛山528000

出　　处：《计算机工程》2014年第8期302-309,共8页Computer Engineering

基　　金：广东省自然科学基金资助项目(10152800001000016);2011年佛山市科技发展专项基金资助项目(2011AA100061)

摘　　要：严格实时系统行为的实时性要求具有不可更改性,非严格实时系统的实时性要求则具有延缓性、替代性以及可补偿性特征,现有的形式化规格说明语言多集中在对严格实时系统的研究,对非严格实时系统的这些特征则缺乏描述能力。针对上述问题,使用一种Object-Z扩展语言来描述非严格实时系统,该方法采用扩展的Object-Z历史不变式表达责任策略,能有效地描述非严格实时系统中的缺省策略、补偿策略以及其他非严格实时策略。以会议系统为例,说明该方法能形式化描述非严格实时行为,具有较强的实用性。Real-time behavior requirements of hard real-time system cannot be changed,however,the real-time behavior requirements of soft real-time systems can be delayed,replaced or compensated.Most current formal specification languages focus on the researches of the hard real-time system,and cannot describe the characteristics of soft real-time system perfectly.To resolve above problems,this paper tries to use a kind of extended language based on Object-Z to describe soft real-time system,which expresses obligation policies by extended object-Z history invariants,and the language can precisely describe the default policies,the compensation policies and the other soft real-time policies in soft real-time system.The example of a meeting system shows,the method can preferably specify soft real-time behaviors formally and has a good applicability.

关 键 词：非严格实时系统 形式化规格说明 责任策略 分布式时态逻辑 Object-Z语言 历史不变式 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]