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

摘要：

复杂实时系统的验证问题一直备受关注.验证过程中,验证特性可以用时序逻辑来描述,但时序逻辑对于非专业人员而言较为复杂,难度较大.观察者模式是一个额外的子系统,可以将复杂的验证特性转换为简单的可达性问题,同时也可以避免使用复杂的验证算法.将Etienne和Nouha Abid等人提出的抽象的观察者模式应用到实时系统实例——Train-Gate系统中,采用UPPAAL工具对Train-Gate系统中的某些场景建立观察者模型,并采用对比实验将验证结果与无观察者模式状态下的验证结果进行对比.对比结果表明,使用观察者模式和验证特性都可以得到正确的验证结果,但观察者更节省时间,对于非专业人员而言更简单且更容易接受.因此,使用观察者模式对如Train-Gate的实时系统进行验证是可行的.

关键词：观察者模式、实时系统、UPPAAL、Train-Gate、模型检测

所属期刊栏目：44

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2018-04-02（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：156-162,174