集成实时逻辑与Z++语言的形式化方法

Formal method of integrating real-time logic and Z++

Lano提出了一种用形式化方法RTL与Z++结合来建模实时系统的方法,并对RTL进行扩展,增强了RTL的表达能力,但对于时间要求非常严格的系统,有时并不能满足系统实时性的要求。可以进一步结合A.K.Mok方法,对表达系统时间约束的RTL公式进行优化,然后再转化为Z++类history中RTL公式,使history中的谓词公式更简要更完整,从而减少了检测时间,提高实时响应能力。

Lano proposed the combination of formal methods RTL and Z＋＋ to modeling real-time systems, and extended the RTL, so as to enhance the ability to express RTL. However when formalized modeling the restrict time requirement systems, it could not satisfy the systematic real-time requirements sometimes. So the method of A. K. Mok can be integrated with it further, and optimizes the RTL formulae expressing timing constraints of the system. Finally the constraints could be translated into RTL formulae of the history of Z＋＋ class. The Optimizing arithmetic will makepredications expressing in RTL formulae of history become more perfect and brief. As a result it reduces the time of monitoring, improves the responsibility.