论文部分内容阅读
混成系统(Hybrid System)是一类常常作为精密仪器的核心控制部件而出现在一些航空航天及列车控制等领域中复杂的系统。因此研究这种核心的控制部件的安全性显得极其重要。混成系统的最为主要的设计建模语言是混成自动机,目前的研究也主要在于检验混成自动机的所具有的安全性上。混成自动机不仅包括了离散性质的变化,还包括了连续性质的变化,而这种连续性质的变化又往往是非线性的,导致混成自动机的验证的复杂度很高。对于小规模的线性系统,验证的方法尝试遍历所有状态空间,以达到安全性检验的目的。但是如果混成自动机状态空间很大,验证无法进行处理。目前现有的工作无法对规模比较大的复杂系统进行验证,即使是线性混成自动机(linear hybrid automata,LHA),复杂系统中比较简单的一种,也无法验证它的可达性问题。验证的方法无法解决上述问题,目前在相关领域基于测试的方法来检验混成自动机的安全性的相关工作已经展开,不过这种基于测试的方法主要是检测状态空间中的某些目标点是否可达。实际工业应用中不仅要检测某些目标点是否可达,同时也要检测某些场景是否可以实现。本文在之前测试技术的基础上,提出了面向场景的混成自动机的测试用例生成的方法,设计与实现了相应的原型工具,进行了实例研究。本文的主要研究工作如下:·提出了面向场景的非线性单自动机测试用例的生成技术。通过用户输入的混成自动机模型,本文构建一个离散搜索图,并在图形上构建一条引导性的区域。本文提出了新的引导性区域生成算法,一方面满足场景事件约束的要求,另外一个方面达到目标控制模式。在这样的引导性区域的指引下,系统可以在混成自动机中进行搜索,查看场景约束的事件是否能够发生。如果满足场景约束条件,并且系统达到目标点,算法会得出最终的测试的用例。·提出了面向场景的多自动机的测试用例的生成技术。实际系统很多都是由多个混成自动机组成的。系统将不同的单一的混成自动机通过共享事件联系起来,使得不同的自动机之间也可以进行交互。因为相互之间关联的引入以及同步事件的时间要求,引入了多自动机的情况。本文针对此问题,给出了面向场景的多自动机的测试用例生成的方法,并且生成了多自动机的测试用例。·应用上述技术,开发了一个面向场景的混成自动机测试用例生成的原型工具,并且进行了实例研究。它可以处理面向场景的单自动机与多自动机的情况,并且可分别生成相应的测试用例。