基于观察者模式的实时系统验证方法  

Real-time System Verification Approach Based on Observer Patterns

作　　者：赵鹤[1] 洪玫[1] 杨秋辉[1] 高婉玲 ZHAO He;HONG Mei;YANG Qiu-hui;GAO Wan-ling(College of Computer Science,Sichuan University,Chengdu610065,China)

机构地区：[1]四川大学计算机学院,成都610065

出　　处：《计算机科学》2017年第12期156-162,174,共8页Computer Science

基　　金：四川省应用基础研究项目:嵌入式系统软件形式化验证技术研究(2014JY0112)资助

摘　　要：复杂实时系统的验证问题一直备受关注。验证过程中,验证特性可以用时序逻辑来描述,但时序逻辑对于非专业人员而言较为复杂,难度较大。观察者模式是一个额外的子系统,可以将复杂的验证特性转换为简单的可达性问题,同时也可以避免使用复杂的验证算法。将Etienne和Nouha Abid等人提出的抽象的观察者模式应用到实时系统实例——Train-Gate系统中,采用UPPAAL工具对Train-Gate系统中的某些场景建立观察者模型,并采用对比实验将验证结果与无观察者模式状态下的验证结果进行对比。对比结果表明,使用观察者模式和验证特性都可以得到正确的验证结果,但观察者更节省时间,对于非专业人员而言更简单且更容易接受。因此,使用观察者模式对如TrainGate的实时系统进行验证是可行的。The verification of complex real-time system is always high-profile.A common way to describe the verification properties is using temporallogic,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 模型检测 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]