使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

带时间约束的LTL性质的模型检测的实现

针对当前的模型检测工具不能对时间自动机直接检测带时间约束的线性时序逻辑性质的问题,对带时间约束的线性时序逻辑性质的模型检测进行了研究。带时间约束的线性时序逻辑公式转Büchi自动机后,性质自动机的迁移边上含有了时间约束,在对性质自动机和模型自动机的复合进行空性检测时,通过使用不同方法对如何获取性质自动机迁移边上的时间约束进行了研究,实现了对带时间约束的线性时序逻辑性质的检测,扩展了工具CATV的检测范围,方便了用户的使用。     

基于实时自动机的连续时段演算的验证

时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解.首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解.与已有工作相比,基于实时自动机设计了验证算法.另外,降低了验证复杂度,并且加速了验证过程的实际速度.     

基于SMT的PTACTL限界模型检测方法

概率时间自动机是在时间自动机的基础上加上各个状态迁移的概率以后形成的一种扩展的时间自动机,能用来对基于时间的随机协议、容错系统等进行建模,具有很强的实用性。本文针对概率时间自动机给出一种基于SMT的限界模型检测方法来验证该模型下的PTACTL性质,该方法由基于SMT的限界模型检测算法演变而来,通过将迁移时间和迁移概率融入ACTL性质中,改变模型的编码以及待验证性质的编码方式来实现对性质的验证。通过2个实例说明检测过程的有效性和高效性。     

AADL分级调度模型的分析与验证

针对嵌入式系统体系结构分析设计语言(architecture analysis and design language,AADL)分级调度模型的分析问题,提出了基于模型检验的可调度性分析和验证方法.基于时间自动机理论,将AADL分级调度模型转换为时间自动机网络,将待验证性质描述为时序逻辑公式,通过模型检验工具对可调度性进行分析和验证.研究结果表明,使用模型检验方法来分析AADL分级调度模型的可调度性是可行的.相对其他方法而言,该方法利用了形式化方法的穷举性来分析系统的性质,分析结果更加精确.     

物联网系统时间自动机建模的研究与应用

探讨基于时间自动机理论进行物联网系统建模和模型检测的理论、方法、工具和实践.对时间自动机的基础理论进行比较全面和精确的论述,完善部分概念及其精确的形式化定义.提出基于时间自动机理论进行建模的方法,并指出时间自动机理论研究对物联网系统建模的指导意义.介绍时间自动机的建模工具UPPAAL,说明基于UPPAAL建立时间自动机模型的建模、仿真和检测方法.结合物联网系统中一个经典的温度感知服务的系统需求、理论与实践相结合,进行温度感知管理系统时间自动机建模,并进行模型仿真与模型检测.实验结果表明,该系统能够正确感知温度,具有容错性且不会陷入死锁.     

基于限界模型检查的Web服务行为失配检测

在Web服务组合过程中,常因交互协议不一致等导致服务失配;Web服务失配检测可准确捕捉失配点,为实现服务的有效组合奠定基础。采用限界模型检查技术,提出一种基于可满足性模理论(SMT)的Web服务行为失配检测方法。该方法首先将服务失配检测问题转化为逻辑公式的可满足性判定问题,然后利用Yices工具实现Web服务行为失配检测,最后通过实例进一步阐述该方法的有效性。     

有穷机和逻辑结合的电子商务协议分析方法

提出一种扩展的有穷自动机模型,并结合卿-周逻辑给出一种新的电子商务协议形式化分析方法,用于分析电子商务协议的可追究性、公平性和时限性.该方法结合了模型检测和逻辑分析两种形式化分析方法的优点,可以准确形象地描述协议的具体运行过程,并且在发生重放攻击时能够正确分析各方的责任.利用该方法对Kim等人提出的改进版ZG协议进行了实例分析,给出了描述该协议运行过程的状态转换图,结合状态转换图对该协议分析得出其满足可追究性、公平性、时限性,并且不存在被重放攻击的可能.最后用时间自动机UPPAAL验证了新方法中有穷自动机模型的准确性和时限性分析的有效性.     

基于时间Petri网的嵌入式系统中断建模与验证

嵌入式系统为中断驱动系统,但中断触发的随机性和不确定性导致中断缺陷很难被追踪发现,并且一旦发生中断故障,往往会使整个嵌入式系统陷入崩溃。因此必须保证中断系统软件的可信性,但是目前缺乏有效的中断系统资源冲突检测方法。针对上述问题,文中首先提出了一种基于时间Petri网的中断系统建模方法,其能够对中断的并发性和时间序列进行有效建模。然后,为方便后续形式化验证,将时间Petri网模型转化为与之等价的时间自动机模型,并提出一种符号编码方法对时间自动机进行形式化编码,将系统模型与所需验证性质编码为一阶谓词逻辑公式,从而能够通过SMT对时间自动机的不变属性进行BMC验证。最后,通过SMT求解器Z3进行实验,实验结果证明了所提方法的有效性。     

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

SAT–LP–IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata

As discrete jumps and continuous flows tangle in the behavior of linear hybrid automata (LHA), the bounded model checking (BMC) for reachability of LHA is a challenging problem. Current works try to handle this problem by encoding all the discrete and continuous behaviors in the bound into a set of SMT formulas which can then be solved by SMT solvers. However, when the system size is large, the object SMT problem could be huge and difficult to solve. Instead of encoding everything into one constraint set, this paper proposes a SAT–LP–IIS joint-directed solution to conduct the BMC for reachability of LHA in a layered way. First, the bounded graph structure of LHA is encoded into a propositional formula set, and solved by SAT solvers to find potential paths which can reach the target location on the graph. Then, the feasibility of certain path is encoded into a set of linear constraints which can then be solved by linear programming (LP) efficiently. If the path is not feasible, irreducible infeasible set (IIS) technique is deployed to locate an infeasible path segment which will be fed to the SAT solver to accelerate the enumerating process. Experiments show that by this SAT–LP–IIS joint-directed solution, the memory usage of the BMC of LHA is well-controlled and the performance outperforms the state-of-the-art SMT-style competitors significantly.     

改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.     

改进的以SMT为基础的实时系统限界模型检测

基于SAT的限界模型检测在处理实时系统时具有很高的复杂度.SMT求解器在计算可满足性的同时,还能处理算术和其他可判定性理论.在对实时系统进行检测时,用SMT求解器代替SAT求解器,系统里的时钟就可以用整型或实型变量表示,时钟约束则可以直接表示成线性算术表达式,从而使整个检测过程更加高效.带时间参数的计算树逻辑(timed computation tree logic,简称TCTL)被用来描述实时系统里的性质.同时,还对检测方法作了相应的改进.     

Modeling and verification of real-time embedded systems with urgency

Real-time embedded systems are often designed with different types of urgencies such as delayable or eager, that are modeled by several urgency variants of the timed automata model. However, most model checkers do not support such urgency semantics, except for the IF toolset that model checks timed automata with urgency against observers. This work proposes an Urgent Timed Automata (UTA) model with zone-based urgency semantics that gives the same model checking results as absolute urgency semantics of other existing urgency variants of the timed automata model, including timed automata with deadlines and timed automata with urgent transitions. A necessary and sufficient condition, called complete urgency, is formulated and proved for avoiding zone partitioning so that the system state graphs are simpler and model checking is faster. A novel zone capping method is proposed that is time-reactive, preserves complete urgency, satisfies all deadlines, and does not need zone partitioning. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.     

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

Predicate diagrams for the verification of real-time systems

This article discusses a new format of predicate diagrams for the verification of real-time systems. We consider systems that are defined as extended timed graphs, a format that combines timed automata and constructs for modelling data, possibly over infinite domains. Predicate diagrams are succinct and intuitive representations of Boolean abstractions. They also represent an interface between deductive tools used to establish the correctness of an abstraction, and model checking tools that can verify behavioral properties of finite-state models. The contribution of this article is to extend the format of predicate diagrams to timed systems. We establish a set of verification conditions that are sufficient to prove that a given predicate diagram is a correct abstraction of an extended timed graph; these verification conditions can often be discharged with SMT solvers such as CVC-lite. Additionally, we describe how this approach extends naturally to the verification of parameterized systems. The formalism is supported by a toolkit, and we demonstrate its use at the hand of Fischer’s real-time mutual-exclusion protocol.     

A survey of timed automata for the development of real-time systems

Timed automata are a popular formalism to model real-time systems. They were introduced two decades ago to support formal verification. Since then they have also been used for other purposes and a large number of variants has been introduced to be able to deal with the many different kinds of requirements of real-time system development. This survey attempts to introduce a massive and complicated theoretical research area to a reader in an easy and compact manner. One objective of this paper is to inform a reader about the theoretical properties (or capabilities) of timed automata which are (or might be) useful for real-time model driven development. To achieve this goal, this paper presents a survey on semantics, decision problems, and variants of timed automata. The other objective of this paper is to inform a reader about the current state of the art of timed automata in practice. To achieve the second aim, this article presents a survey on timed automata’s implementability and tools.     

一种基于离散时间自动机的LTL性质检测工具

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。