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

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

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

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

时间自动机与信号自动机的互模拟算法

基于时间自动机的验证工具已被广泛应用于实时系统模型验证。信号自动机为一类实时系统建立了比时间自动机更适合的模型,但是它还不能用于实际的实时系统模型验证,因为没有验证算法可用。把信号自动机验证问题归约到了时间自动机验证问题：证明了两种自动机具有相同的识别语言能力,证明了二者具有双向模拟关系,并在此基础上提出了线性的互模拟算法。把互模拟算法和已有的时间自动机验证算法结合起来,就得到了信号自动机的验证算法,从而解决了对信号自动机模型的验证问题。     

时间ω-树自动机识别语言的一个条件

时间自动机被广泛用于实时系统验证和模型检验.为适应不同类型的系统验证需要,不少时间自动机的相关模型被提出.时间树自动机是这样的新模型之一.目前主要是针对时间树自动机识别的语言类及相关性质的研究.本文提出了时间树自动机识别语言的一个条件,并证明了结论的正确性.如果一个语言不能满足该条件,它一定不能被时间树自动机识别.这为证明一个具体语言不能被时间树自动机识别提供了思路.     

一种基于时间自动机网络的实时系统形式化验证方法

介绍了时间自动机形式模型,在此基础上给出了时间自动机网络的形式语法和语义,然后给出一种基于时间自动机网络的实时系统形式化验证方法,并采用基于时间自动机网络的模型检测工具UPPAAL对一个经典的实时系统实例进行了验证．     

一种基于UPPAAL的智能合约属性形式化验证方法

针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性,再使用模型检测工具UPPAAL验证智能合约的属性;最后对购物合约进行了建模与验证,验证了该方法的有效性.     

一种时间自动机时钟离散化算法

稠密时间自动机被广泛应用于实时系统自动验证.然而其在补操作下不封闭,因而导致多种线性实时性质不可验证.离散时间自动机虽不存在此问题,但该模型表达能力偏弱.因此,提出了一种时间自动机时钟离散化算法,结合时钟物理约束因素,证明了新方法可有效解决上述问题.     

矿井机车自主驾驶过程的建模及验证

文章首先使用自然语言描述了矿井机车自主驾驶系统的结构和控制过程;然后基于时间自动机理论对自主驾驶中涉及的机车控制器、机车运行服务器以及其他车载设备、被控对象建模,从而得到自主驾驶的时间自动机网络模型;最后应用时间自动机模型验证工具UPPAAL对自主驾驶模型进行了仿真分析和验证。验证结果表明建立的模型满足系统的功能性需求和实时性需求,证明了系统设计的正确性。     

时间自动机与自动验证

给出时间自动机的基本概念,描述了区域自动机的构造方法,并且实现了区域自动机的构造算法.简述了通过时间自动机进行自动验证的过程,最后分析了区域自动机构造算法的时间复杂度.     

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

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