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

摘要：

严格实时系统行为的实时性要求具有不可更改性,非严格实时系统的实时性要求则具有延缓性、替代性以及可补偿性特征,现有的形式化规格说明语言多集中在对严格实时系统的研究,对非严格实时系统的这些特征则缺乏描述能力.针对上述问题,使用一种Object-Z扩展语言来描述非严格实时系统,该方法采用扩展的Object-Z历史不变式表达责任策略,能有效地描述非严格实时系统中的缺省策略、补偿策略以及其他非严格实时策略.以会议系统为例,说明该方法能形式化描述非严格实时行为,具有较强的实用性.

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

所属期刊栏目：40

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2014-09-15（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：302-309