结合关注事件的时间自动机语言包含模型检测

Language Inclusion Checking of Timed Automata with Concerned Events

时间自动机是实时系统形式化建模和验证的主要手段,能够对系统各个组件能否正确交互及通信进行验证.系统模型和待验证属性都用时间自动机表示,时间自动机语言包含模型检测方法能够验证系统模型是否满足带有时间要求的属性.目前相关工作中没有完善的能够应用于实际的语言包含检测方法,因为该方法要求系统模型和验证属性具有相同的事件集合,但在实际问题中,系统模型往往包含大量事件,而属性模型一般只关注少数的事件.因此,本文改进了已有的时间自动机语言包含算法,使其在运行时只需考虑关注事件,并总结了时间自动机描述的常用属性模式,以帮助用户更好地建模.此外,本文将该方法用于一个水位控制系统的建模和验证,得出了有效结论.

Timed automata are the primary method for formal modeling and checking of real-time systems.They can also check whether various components of the system are correctly interacting and communicating.Both the system models and the properties to be verified are represented by timed automata.The language inclusion checking of timed automata can check whether the system model satisfies given properties with time.At present,there is no perfect language inclusion checking method to be applied to the actual system.Because the method needs system models and properties to be verified have the same set of events.However,in practical problems,system models often contain a large number of events,while properties generally only need to pay attention to a few events.Therefore,we improve the existing timed automata language inclusion checking algorithm so that it only needs to consider the concerned events.And then,we summarize the common property patterns described by timed automata.In addition,the method is applied to a water level control system with effective conclusion.