可更新Datalog的分布式时态逻辑扩展及应用

针对现有的分布式逻辑语言缺乏完整时态表达力等问题,将分布式时态逻辑谓词引入Datalog规则,提出TU-Datalog语言。该语言通过融入U-Datalog的非即时性更新语义,形成完全声明式具有强大时态表达力的逻辑编程语言和环境。通过扩展U-Datalog逻辑固定点语义,提出TU-Datalog语言的固定点时态演化规则,并对该语言的语法、语义、评价算法进行了研究,最后对该语言的应用做了说明和示例。

DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述

Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描述操作的时态驱动、事件驱动、操作补偿等因素,分析和说明了该语言的语法和语义,最后通过对责任授权模型的形式化描述说明了该语言的表达能力和应用。

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

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