作　　者： ; ;

机构地区： 广东工业大学计算机学院

出　　处： 《计算机工程与设计》 2005年第11期2887-2890,共4页

摘　　要： 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.

关 键 词： 实时逻辑 形式化方法 约束图 时间约束

领　　域： [自动化与计算机技术] [自动化与计算机技术]