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

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