基于接口自动机的嵌入式软件验证技术及支撑工具研究

发布时间：2020-12-12 05:08

　　现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术。由于嵌入软件具有极高的可靠性、严格的实时性以及资源、能耗使用的受限性,使得保证系统设计满足给定的功能规约以及满足非功能方面的严格限制成为嵌入式计算领域中的重要研究课题。传统的嵌入式软件可靠性保障技术主要关注于系统开发后期,而在系统设计前期缺乏有效工具对系统设计的功能性质以及非功能性质进行分析与验证。本文以接口自动机及其扩展模型作为构件化嵌入式软件的设计模型,以UML顺序图描述基于场景的功能规约,对基于接口自动机及其扩展模型的多个模型检验抽象算法进行分析且设计相应的算法实现框架。进而在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD（Tool for Component-Based Embedded Software Design）。该工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题;另外,对非实时资源使用相关性... 

【文章来源】：南京航空航天大学江苏省 211工程院校

【文章页数】：76 页

【学位级别】：硕士

【部分图文】：

Communication的接口自动机模型

从信道返回的ack；然后向调用者返回通信失败：fail。从图中可以看出，Comm入动作msg仅在状态0可以接受，在其余用了msg方法，则在下一次调用msg之前nication被另外一个构件User使用(如图2.2失败的处理。这样，总是返回ok就成为了图 2.1 Communication 的接口自动机模型

图 3.1 TCAS 系统中飞行冲突探测场景的 UML 顺序图中的消息发送以及消息的接收都使用事件来表示。不失一般性，假定每或多个可视序列，每个可视序列中的元素都是一个事件对(e1, e2) ；表示生。在本文中，暂不考虑带选择分支的顺序图。在图中只要当出现满足被视为在事件e2之前发生：果关系：e1为消息发送事件，e2为此消息对应的接收事件。制关系：在同一个构件的生命线轴上，事件e1出现于事件e2的上方，且e2事件顺序表明一个发送事件可以等待其他事件的发生。但是一个构件只件的时间先后，对于接收消息事件，由于系统的底层结构和消息传送的收消息的时间也是不确定的，所以对消息接收事件的发生的顺序没有做O顺序关系：在同一个构件的生命线轴上，接收事件e1出现于接收事件的发送事件'1e 和'2e 同时出现在另外一个构件的生命线轴上，且'1e 位置高序图中的任何消息而言，可能是同步的，也可能是异步的。异步的消息则在其发送和接收事件之间不会有时间延迟。本文中假定顺序图中的消

【参考文献】：
期刊论文
[1]构件化嵌入式软件设计的能耗性质分析与验证[J]. 曹东,胡军,徐丙凤.  南京理工大学学报(自然科学版). 2009(01)
[2]网构软件的资源自适应性的形式化分析与验证[J]. 胡军,黄志球,曹东,徐丙凤.  软件学报. 2008(05)
[3]基于场景规约的构件式系统设计分析与验证[J]. 胡军,于笑丰,张岩,王林章,李宣东,郑国梁.  计算机学报. 2006(04)
[4]基于场景构件式实时软件设计的一致性检验[J]. 胡军,于笑丰,张岩,李宣东,郑国梁.  软件学报. 2006(01)
[5]嵌入式软件建模、实现与验证:研究与进展[J]. 胡军,张岩,于笑丰,王林章,李宣东,郑国梁.  计算机科学. 2005(12)
[6]接口自动机——一种用于组件组合的形式系统[J]. 张岩,胡军,于笑丰,李宣东,郑国梁.  计算机科学. 2005(11)
[7]软件复用与软件构件技术[J]. 杨芙清,梅宏,李克勤.  电子学报. 1999(02)

博士论文
[1]构件化嵌入式软件设计的分析与验证[D]. 胡军.南京大学 2005



本文编号：2911911