基于观察者模式的实时系统验证方法
Real-time System Verification Approach Based on Observer Patterns
赵鹤 1洪玫 1杨秋辉 1高婉玲1
作者信息
摘要
复杂实时系统的验证问题一直备受关注.验证过程中,验证特性可以用时序逻辑来描述,但时序逻辑对于非专业人员而言较为复杂,难度较大.观察者模式是一个额外的子系统,可以将复杂的验证特性转换为简单的可达性问题,同时也可以避免使用复杂的验证算法.将Etienne和Nouha Abid等人提出的抽象的观察者模式应用到实时系统实例——Train-Gate系统中,采用UPPAAL工具对Train-Gate系统中的某些场景建立观察者模型,并采用对比实验将验证结果与无观察者模式状态下的验证结果进行对比.对比结果表明,使用观察者模式和验证特性都可以得到正确的验证结果,但观察者更节省时间,对于非专业人员而言更简单且更容易接受.因此,使用观察者模式对如Train-Gate的实时系统进行验证是可行的.
Abstract
The verification of complex real-time system is always high-profile.A common way to describe the verification properties is using temporal logic,and the way is complex and difficult for laypeople.Observer patterns is an additional subsystem.It can transform the complex verification properties into simple reachability problem.The use of observer patterns can avoid using complex verification algorithm.The observer patterns proposed by Etienne and Nouha Abid were applied to the real-time system,Train-Gate system.UPPAAL was used to construct the observer models according to some scenarios in Train-Gate.Comparative experiment was used to compare the verification result with and without observer patterns.The experiment result shows that the use of observer patterns and verification properties both can get correct results.And the use of observer patterns can save time and it's easier to accept for laypeople.Therefore,the use of observer patterns is feasible in the real time systems like Train-Gate verification.
关键词
观察者模式/实时系统/UPPAAL/Train-Gate/模型检测Key words
Observer patterns/Real-time system/UPPAAL,Train-Gate/Model checking引用本文复制引用
基金项目
四川省应用基础研究项目(2014JY0112)
出版年
2017
NETL
NSTL
维普
万方数据