Abstract: 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.

Key words: soft real-time system, formal specification, obligation policy, distributed temporal logic, Object-Z language;history invariant

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

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

CLC Number: 

• TP311