APTL公式的可满足性检查工具

交替投影时序逻辑（Alternating Projection Temporal Logic,简称APTL）公式简单易懂,表达能力强;不仅可以描述经典时序逻辑LTL可以描述的性质,而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在验证系统是否满足所给的APTL公式所描述的性质之前需要检查公式的可满足性.本文根据检查APTL公式的可满足性的方法^[1],开发实现了工具APTL2BCG.具体细节如下：首先,利用公式P的范式构造P的标记范式图（Labeled Normal Form Graph,简称LNFG）;然后,将LNFG转化为广义的基于并发博弈结构的交替Büchi自动机（Generalized alternating Büchi automaton over Concurrent Game structure,简称GBCG）;最后,将GBCG转化为基于并发博弈结构的交替Büchi自动机（alternating Büchi automaton over Concurrent Game structure,简称BCG）并且化为最简形式并检查公式P的可满足性.     

三机冗余容错系统的描述和验证

使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessor_P刻画程序P在单机上运行,用时序逻辑式Spec_P刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessors_P即使在出现硬件错误的情况下运行,也能满足性质Spec_P.     

命题线性时序逻辑的对偶模型问题的复杂性

定义了一个命题线性时序逻辑的对偶模型的概念.一个公式f的对偶模型是指f的满足以下条件的两个模型(即状态的w序列):在每个位置上这两个模型对原子命题的赋值都是对偶的.然后,对于确定一个公式f是否有对偶模型的判定问题(记为DM)和在一个Kripke-结构中确定是否存在从两个给定状态出发的对偶模型满足给定公式f的判定问题(记为KDM)的复杂性进行了研究.证明了以下结果:对于只含有F("Future")算子的命题线性时序逻辑,DM和KDM都是NP完全的;而对于以下命题线性时序逻辑,DM和KDM都是PSPACE完全的:含有F,X ("Next")算子的逻辑、含有U("Until")算子的逻辑、含有U,S,X算子的逻辑以及由Wolper给出的含有正规语言算子的逻辑(一般称为扩展时序逻辑,简称ETL).     

一个命题投影时序逻辑符号模型检测器

现有模型检测工具的形式化规范语言,如计算树逻辑(computation tree logic,简称CTL)和线性时序逻辑(linear temporal logic,简称LTL)等的描述能力不足,无法验证ω正则性质.提出了一个命题投影时序逻辑(propositional projection temporal logic,简称PPTL)符号模型检测工具——PLSMC(PPTL symbolic model checker)的设计与实现过程.该工具基于著名的符号模型检测系统NuSMV,实现了PPTL的符号模型检测算法.PLSMC的规范语言PPTL具有完全正则表达能力,这使得定性性质和定量性质均可被验证.此外,PLSMC可以有效地缓解模型检测工具中容易发生的状态空间爆炸问题.最后,利用PLSMC对铁路公路交叉道口护栏控制系统的安全性质和周期性性质进行验证.实验结果表明,PPTL符号模型检测工具扩充了NuSMV系统的验证能力,使得时间敏感、并发性和周期性等实时性质可以被描述和验证.     

有界模型检测的优化

G(p)和G(p→F(q))是有界模型检测(bounded model checking,简称BMC)中的两个重要的常用模态算子.对验证G(p)和G(p→F(q))编码转换公式进行优化.通过分析当验证这些模态算子时FSM(finite state machine)的状态转移和线性时序逻辑(linear-time temporal logic,简称LTL)的语义特征.在现有的编码公式的基础上,给出了简洁、高效的递推公式,该公式有利于高效编码成SAT(satisfiability)实例;证明了递推公式和原转换公式的逻辑关系.通过实验比较分析,在生成SAT实例规模和易求解方面都优于BMC中求解这些模态算子的现有的两种重要方法AA_BMC和Timo_BMC.所给出的方法和思想对于BMC中验证其他模态算子时的编码优化也有参考价值.     

不可满足公式的同态证明系统

合取范式(CNF)公式H到F的同态φ是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.     

QRDChecker:一个QRDC模型检验工具

反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.     

高阶类型化可验证应用系统体系结构建模及案例

随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计无法支持需求满足验证,需求满足验证需要其它验证工具的支持.而应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.本文面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下,提出了一种高阶类型化模型驱动的可验证应用系统体系结构建模语言（V_ASAML）与可验证应用系统体系结构建模方法（V_ASAMM）.V_ASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ⊦t：T和Γ⊦R（T₁,T₂）是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.V_ASAMM方法给出了应用系统体系结构建模过程,包括构建M_bd（基本数据类型）、M_bti（基本接口类型）、M_dev（设备类型）和M_frwk（应用系统框架）等四层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图（G_DSI）用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统V_ASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.     

基于XYZ/E描述和验证容错系统

研究使用XYZ/E描述和验证容错系统.基于XYZ/E中可执行程序P对应的状态转换系统对其错误环境F建模,通过错误转换给出错误影响程序P_F;基于P,F和恢复算法R,通过容错转换给出容错程序P_F-R;定义了程序P,Q之间两种求精关系:容错求精和向后恢复求精,基于这两种求精关系可直接从程序P的规范推导出程序Q满足的一些性质.     

一种基于Büchi自动机的LTL程序模型检测方法

时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。基于自动机的理论,用标签转移系统（S）表示程序的行为,用时序逻辑公式（F）描述程序的性质,构建相应的Büchi自动机,从而证明形式化公式SF是否可满足。     

The Saga of Synchronous Bus Arbiter: On Model Checking Quantitative Timing Properties of Synchronous Programs

Quantified Discrete-time Duration Calculus, (QDDC), is a form of interval temporal logic [14]. It is well suited to specify quantitative timing properties of synchronous systems. An automata theoretic decision procedure for QDDC allows converting a QDDC formula into a finite state automaton recognising precisely the models of the formula. The automaton can be used as a synchronous observer for model checking the property of a synchronous program. This theory has been implemented into a tool called DCVALID which permits model checking QDDC properties of synchronous programs written in Esterel, Verilog and SMV notations.In this paper, we consider two well-known synchronous bus arbiter circuits (programs) from the literature. We specify some complex quantitative properties of these arbiters, including their response time and loss time, using QDDC. We show how the tool DCVALID can be used to effectively model check these properties (with some surprising results).     

Beyond vacuity: towards the strongest passing formula

Given an LTL formula φ in negation normal form, it can be strengthened by replacing some of its literals with false. Given such a formula and a model M that satisfies it, vacuity and mutual vacuity attempt to find one or a maximal set of literals, respectively, with which φ can be strengthened while still being satisfied by M. We study the problem of finding the strongest LTL formula that satisfies M and is in the Boolean closure of strengthened versions of φ as defined above. This formula is stronger or equally strong to any formula that can be obtained by vacuity and mutual vacuity. We present our algorithms in the framework of lattice automata.     

Using heuristic search for finding deadlocks in concurrent systems

Model checking is a formal technique for proving the correctness of a system with respect to a desired behavior. This is accomplished by checking whether a structure representing the system (typically a labeled transition system) satisfies a temporal logic formula describing the expected behavior. Model checking has a number of advantages over traditional approaches that are based on simulation and testing: it is completely automatic and when the verification fails it returns a counterexample that can be used to pinpoint the source of the error. Nevertheless, model checking techniques often fail because of the state explosion problem: transition systems grow exponentially with the number of components. The aim of this paper is to attack the state explosion problem that may arise when looking for deadlocks in concurrent systems described through the calculus of communicating systems. We propose to use heuristics-based techniques, namely the A* algorithm, both to guide the search without constructing the complete transition system, and to provide minimal counterexamples. We have realized a prototype tool to evaluate the methodology. Experiments we have conducted on processes of different size show the benefit from using our technique against building the whole state space, or applying some other methods.     

Combining Local and Global Model Checking

The verification process of reactive systems in local model checking [1,7] and in explicit state model checking is[13,15] on-the-fly. Therefore only those states of a system have to be traversed that are necessary to prove a property. In addition, if the property does not hold, than often only a small subset of the state space has to be traversed to produce a counterexample. Global model checking [6,23] and, in particular, symbolic model checking [4,22] can utilize compact representations of the state space, e.g. BDDs [3], to handle much larger designs than what is possible with local and explicit model checking. We present a new model checking algorithm for LTL that combines both approaches. In essence, it is a generalization of the tableau construction of [1] that enables the use of BDDs but still is on-the-fly.     

Local Module Checking for CTL Specifications

Model checking is a well known technique for the verification of finite state models using temporal logic specification. While model checking is suitable for transformational systems (also called closed systems), it is unsuitable for open systems (also known as reactive systems) where the nondeterminism in the environment must be considered during verification. Module checking is an approach for the verification of open systems which have both closed (internal) and open (environment or external) states. It has been demonstrated in [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module checking. Information and Computation, 164:322–344, 2001] that the complexity of module checking branching time logic CTL is EXPTIME-complete. The approach to module checking is global and the method tries to establish that the property in question holds over all possible environments.This papers develops a local approach to CTL module checking using tableau rules. The proposed approach tries to determine a single environment under which the negation of the property is satisfied over the given module. Such a strategy, thus, leads to a local approach to module checking where we only explore states that are relevant to proving that the negation of the property can be satisfied over the given module using an appropriate witness (environment) that the algorithm also generates. While the worst case complexity of our algorithm is identical to the earlier complexity, we demonstrate that practical implementation of the proposed approach is feasible and yields much better results than the global approach.     

Pragmatics of model checking: an STTT special section

Since its discovery in the early 1980s, model checking has emerged as one of the most exciting areas in the field of formal verification of system correctness. The chief reason for this enthusiasm resides in the fact that model checkers establish in a fully automated manner whether or not a system satisfies formal requirements; users need not construct proofs. Until the early 1990s, however, the practical impact of model checking was modest, in large part because the state-explosion problem limited the applicability of the technology. Recent advances in the field have dramatically expanded the scope of model checking, however, and interest in it on the part of practitioners is growing. This special section surveys several recent approaches to attacking the state explosion that are supporting the continued advancement of model checking as a viable technology for improved system design.     

Component Verification with Automatically Generated Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work introduces an approach that brings a new dimension to model checking of software components. When checking a component against a property, our modified model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of two NASA applications.This paper is an expanded version of Giannakopoulou et al. (2002).     

From liveness to promptness

Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bound on the “wait time” for an eventuality to be fulfilled. That is, F θ asserts that θ holds eventually, but there is no bound on the time when θ will hold. This is troubling, as designers tend to interpret an eventuality F θ as an abstraction of a bounded eventuality F ^≤k θ, for an unknown k, and satisfaction of a liveness property is often not acceptable unless we can bound its wait time. We introduce here prompt-LTL, an extension of LTL with the prompt-eventually operator F _p . A system S satisfies a prompt-LTL formula φ if there is some bound k on the wait time for all prompt-eventually subformulas of φ in all computations of S. We study various problems related to prompt-LTL, including realizability, model checking, and assume-guarantee model checking, and show that they can be solved by techniques that are quite close to the standard techniques for LTL.     

Modular abstractions for verifying real-time distributed systems

In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well.The specification languageRTL is a branching-time version of the real-time temporal logicTPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage ofRTL.