采用模型检测器的软件安全模型验证方法

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.     

序列图建模机理与应用研究

研究了序列图在软件设计中的应用问题,解析了其组成和表示,探索了其对象的交互机理和交互原则,分析了其本质与在MDA软件范型中的建模应用,诸如用序列图表示的模型转换性和可追溯性,讨论了序列图与面向对象编程的内在联系.     

应用UML2.0模型的测试用例生成方法

针对软件开发过程中测试自动化程度低的问题,在研究基于模型的测试用例生成技术的基础上,提出了一种基于UML2.0序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证了自动机模型的正确性.使用自动机模型与用例描述来生成测试用例,该用例满足事件与全路径覆盖准则.通过对图书管理系统的分析表明,该方法不仅能够提高软件的测试效率,而且还确保了针对管理员的执行动作所产生的测试用例的正确性.     

基于时间自动机的UML模型转换与验证研究

针对无法对UML模型进行形式化验证的问题,提出在元模型层将UML模型转换为时间自动机模型并进行验证的方法.形式化UML状态机的结构,抽象出UML和时间自动机的元模型,利用模型转换语言ATL对UML元模型和时间自动机元模型构造映射规则,实现UML模型到时间自动机模型的转换,在模型验证工具Uppaal中对转换结果进行形式化验证.最后进行实例研究,结果表明了此方法的有效性和先进性.     

基于UPPAAL的铁路车站信号联锁系统模型验证

详细介绍了适于描述实时系统的形式化方法,时间自动机以及基于时间自动机的模型验证工具UPPAAL.给出了铁路车站信号系统中的联锁功能进路建立的时间自动机模型,并利用UPPALL对其进行了分析与验证.     

PLC程序形式化的设计与验证

从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.     

基于价格时间自动机的飞机着陆最优成本研究

针对目前航空运输系统中对飞机着陆调度成本效益研究的不足,提出采用价格时间自动机作为形式化描述方法,将飞机着陆过程建模为其相关实体的交互行为,引入时间和价格因素描述各实体的属性和行为,从而将飞机着陆形式化为时间价格的动态交互协作,并分别为相关实体和服务建模,形成彼此独立又相互协作的价格时间自动机网络,将飞机着陆调度成本表示为价格时间自动机网络上的状态转换路径。最后提出一组系统模型需要满足的性质,使用价格时间自动机模拟验证工具UPPAAL CORA仿真并验证其正确性,使用最优成本标准分支算法分析求解飞机着陆调度最优成本的可达性。     

基于时间自动机的嵌入式系统AADL模型可调度性验证

采用时间自动机形式化模型检验方法建立了结构分析与设计语言(AADL)调度模型的自动机,实现了从AADL模型到时间自动机模型的自动转换与验证.首先,设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板,建立了AADL调度模型到时间自动机模型的语义映射法则.然后,设计了自动化模型转换插件,并将其集成到OSATE建模工具中,实现了建模、转换、验证的集成开发环境.最后,利用UPPAAL工具对时间自动机模型进行模拟与验证.仿真实验结果表明,所建立的模型转换方法能够有效、实时地将AADL模型转换为时间自动机模型,并可在UPPAAL中分析原模型的可调度性.     

基于混成自动机的CPS行为建模与属性验证

系统实时性、安全性和可靠性等非功能属性是信息物理系统在诸多领域应用的关键因素。论文在分析CPS模型构建与分析验证中面临的挑战的基础上,提出了一种CPS行为建模与属性验证方法。该方法首先基于混成自动机对CPS的行为进行建模,然后将此模型转换为混合程序模型,最后在定理证明器KeYmaera中对HP模型的属性进行形式化验证。文中论述了行为模型描述语言的结构,建立了混成自动机模型与HP模型之间的转换规则,分析了模型转换的一致性。应用实例表明:该方法既能简单直观地描述CPS动态行为,又能对CPS的属性进行严格的形式化验证,且有效避免了形式化验证中的状态空间爆炸问题。     

业务流程的形式化设计与验证

针对如何保证业务流程设计模型与业务需求的一致性问题,在研究有限自动机模型的基础上,提出了一种业务流程的自动机模型构建和验证方法.采用扩展的带约束条件的确定有限自动机对业务流程设计模型进行形式化描述,使用线性时序逻辑表示业务需求,分别给出业务流程设计模型到自动机模型和自动机模型到Promela描述的转换算法,并通过模型检测技术,使用Spin工具验证设计模型是否满足需求性质.若不满足性质,则能够获得反例执行的路径.实例分析表明,该方法可用于业务流程设计的正确性验证.