一种基于满足性判定的并发软件验证策略

对线性时态逻辑SE-LTL提出了一种基于SAT的有界模型检测过程,该过程避免了基于BDD方法中状态空间快速增长的问题.在SE-LTL的子集SE-LTL?X的有界模型检测过程中,集成了stuttering等价技术,该集成有效地加速了验证过程.进一步提出了一种组合了基于SAT的有界模型检测、基于反例的抽象求精、组合推理3种状态空间约简技术的并发软件验证策略.该策略中,抽象和求精在每一个构件上独立进行.同时,模型检测的过程是符号化的.实例表明,该策略降低了验证时间和对内存空间的需求.     

Distributed Model Checking: From Abstract Algorithms to Concrete Implementations

Distributed Model Checking (DMC) is based on several distributed algorithms, which are often complex and error prone. In this paper, we consider one fundamental aspect of DMC design: message passing communication, the implementation of which presents hidden tradeoffs often dismissed in DMC related literature. We show that, due to such communication models, high level abstract DMC algorithms might face implicit pitfalls when implemented concretely. We illustrate our discussion with a generic distributed state space generation algorithm.     

Model checking: recent improvements and applications

Model checking (Baier and Katoen in Principles of model checking, MIT Press, Cambridge, 2008; Clarke et al. in Model checking, MIT Press, Cambridge, 2001) is an automatic technique to formally verify that a given specification of a concurrent system meets given functional properties. Its use has been demonstrated many times over the years. Key characteristics that make the method so appealing are its level of automaticity, its ability to determine the absence of errors in the system (contrary to testing techniques) and the fact that it produces counter-examples when errors are detected, that clearly demonstrate not only that an error is present, but also how the error can be produced. The main drawback of model checking is its limited scalability, and for this reason, research on reducing the computational effort has received much attention over the last decades. Besides the verification of qualitative functional properties, the model checking technique can also be applied for other types of analyses, such as planning and the verification of quantitative properties. We briefly discuss several contributions in the model checking field that address both its scalability and its applicability to perform planning and quantitative analysis. In particular, we introduce six papers selected from the 23rd International SPIN Symposium on Model Checking Software (SPIN 2016).

     

形式验证中同步时序电路的VHDL描述到S2-FSM的转换

符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ,ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法．由于验证时间和有限状态机模型的大小是直接相关的,因而模型的大小就成为ＳＭＣ中的关键问题．本文提出一种基于同步电路行为描述的新的有限状态机模型Ｓ２－ＦＳＭ,并给出从同步电路的ＶＨＤＬ描述建立这种模型的过程．由于该模型的状态转换函数是基于时钟周期的,消去了与时钟无关的大量中间变量,所以同Ｄｅｈａｒｂｅ提出的模型相比,它的状态数大大减少．若干电路的实验结果表明,该模型由于减少了状态规模,建模时间和可达性分析时间大大减少,效果十分显著．     

Program model checking as a new trend

This paper introduces a special section of the STTT journal containing a selection of papers that were presented at the 7th international SPIN workshop, Stanford, 30 August – 1 September 2000. The workshop was named SPIN Model Checking and Software Verification, with an emphasis on model checking of programs. The paper outlines the motivation for stressing software verification, rather than only design and model verification, by presenting the work done in the Automated Software Engineering group at NASA Ames Research Center within the last 5 years. This includes work in software model checking, testing like technologies and static analysis. Published online: 2 October 2002     

Bounded Model Checking of CTL

Bounded Model Checking has been recently introduced as an efficient verification method for reactive systems. This technique reduces model checking of linear temporal logic to propositional satisfiability. In this paper we first present how quantified Boolean decision procedures can replace BDDs. We introduce a bounded model checking procedure for temporal logic CTL＊ which reduces model checking to the satisfiability of quantified Boolean formulas. Our new technique avoids the space blow up of BDDs, and extends the concept of bounded model checking.     

A vertex centric parallel algorithm for linear temporal logic model checking in Pregel

Linear Temporal Logic (LTL) Model Checking is a very important and popular technique for the automatic verification of safety-critical hardware and software systems, aiming at ensuring their quality. However, it is well known that LTL model checking suffers from the state explosion problem, often leading to insurmountable scalability problems when applying it to real-world systems. While there has been work on distributed algorithms for explicit on-the-fly LTL model checking, these are not sufficiently scalable and capable of tolerating faults during computation, significantly limiting their usefulness in huge cluster environments. Moreover, implementing these algorithms is generally viewed as a very challenging, error-prone task. In this paper, we instead rely on Pregel, a simple yet powerful model for distributed computation on large graphs. Pregel has from the start been designed for efficient, scalable and fault tolerant operation on clusters of thousands of computers, including large cloud setups. To harness Pregel’s power, we propose a new vertex centric distributed algorithm for explicit LTL model checking of concurrent systems. Experimental results illustrate feasibility and scalability of the proposed algorithm. Compared with other distributed algorithms, our algorithm is more scalable, reliable and efficient.     

A Model Checking-based Method for Verifying Web Application Design

Development of Web Applications (WA) needs new methods, techniques and tools to support an engineered project during all the phases of its life cycle. To ensure the reliability of WA it is important they be validated and verified at early design phase. We use Model Checking techniques to perform automated verification of the UML design of a WA.We propose a mathematical model of a WA partitioning the usual Kripke structure into windows, links, pages and actions. Then we specify properties to be checked in a temporal logic, Computation Tree Logic (CTL). Verification is performed adapting the SMV model checker to our formalism. An implemented system that embeds the SMV verifier automatically parses the XMI output of UML tool and builds the SMV model to be verified with respect to specifications. Results of verification proved the benefits of the method.     

VyrdMC: Driving Runtime Refinement Checking with Model Checkers

This paper presents VyrdMC, a runtime verification tool we are building for concurrent software components. The correctness criterion checked by VyrdMC is refinement: Each execution of the implementation must be consistent with an atomic execution of the specification. VyrdMC combines testing, model checking, and Vyrd, the runtime refinement checker we developed earlier. A test harness first drives the component to a non-trivial state which serves as the starting state for a number of simple, very small multi-threaded test cases. An execution-based model checker explores for each test case all distinct thread interleavings while Vyrd monitors executions for refinement violations. This combined approach has the advantage of improving the coverage of runtime refinement checking at modest additional computational cost, since model checkers are only used to explore thread interleavings of a small, fixed test program. The visibility and detailed checking offered by using refinement as the correctness criterion differentiate our approach from simply being a restricted application of model checking. An important side benefit is the reduction in program instrumentation made possible if VyrdMC is built using a model checker with its own virtual machine, such as Java PathFinder [Guillaume Brat, Klaus Havelund, Seung-Joon Park, and Willem Visser. Model Checking Programs. In IEEE International Conference on Automated Software Engineering (ASE), September 2000]. We are investigating the use of two different model checkers for building VyrdMC: Java PathFinder, an explicit-state model checker and Verisoft, a “stateless” model checker [P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 174–186, Paris, January 1997].     

UML模型检测方法的研究

统一建模语言（UML）是设计和分析软件系统最常用的方法，如何保证UML模型满足某些特性是一个非常重要的问题，而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器（SPIN）对UML模型进行检测的方法。首先对UML模型进行形式化描述，使用层次自动机来描述状态图，然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA，使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束，通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。     

Preface of the special issue on Model Checking of Software

Software Model Checking consists of a broad collection of techniques to tackle the complexity and the diversity in the use of software in safety-critical systems. The contributions in this special issue address some of the core problems in software model checking. The articles are based on papers selected from the 2013 SPIN Symposium on Model Checking of Software, an annual forum for practitioners and researchers interested in symbolic and state space-based techniques for the validation and analysis of software systems.     

WAVer: A Model Checking-based Tool to Verify Web Application Design

Web Applications are becoming more and more widespread and efficient, then an increase of their reliability is now strongly required. Hence methods to support design and automatically perform validation of a Web Application (WA) could be helpful. In this paper we present WAVer, a prototype tool for performing the verification of a WA design by means of Symbolic Model Checking techniques. The tool first performs the modeling of the WA and furthermore verify it by means of a model checker. Specifically, the mathematical model of the WA is represented by a Finite State Machine (FSM). Then, by using the CTL formal language, we formalize basic criteria to establish correctness of the application. The prototype system we have implemented embeds a component which automatically imports WA design from a UML tool; CTL specifications are added and translated as source code for NuSMV model checker. Finally, the checker performs verification: if there is a violation of specifications, NuSMV allows to locate errors in WA design and appropriate adjustments are carried out.     

From NuSMV to SPIN: Experiences with model checking flight guidance systems

Model checking has become a promising technique for verifying software and hardware designs; it has been routinely used in hardware verification, and a number of case studies and industrial applications show its effectiveness in software verification as well. Nevertheless, most existing model checkers are specialized for limited aspects of a system, where each of them requires a certain level of expertise to use the tool in the right domain in the right way. Hardly any guideline is available on choosing the right model checker for a particular problem domain, which makes adopting the technique difficult in practice, especially for verifying software with high complexity. In this work, we investigate the relative pitfalls and benefits of using the explicit model checker Spin on commercial Flight Guidance Systems (FGSs) at Rockwell-Collins, based on the author's prior experience with the use of the symbolic model checker NuSMV on the same systems. This has been a question from the beginning of the project with Rockwell-Collins. The challenge includes the efficient use of Spin for the complex synchronous mode logic with a large number of state variables, where Spin is known to be not particulary efficient. We present the way the Spin model is optimized to avoid the state space explosion problem and discuss the implication of the result. We hope our experience can be a useful 21 reference for the future use of model checking in a similar domain.     

身份认证协议的模型检测分析

提出一个直观、易用的模型来模拟和验证身份认证协议，并给出基于Spin(模型检测工具）的实现，它不仅可以模拟多对参与者同时进行会话，而且还有效缩减了状态空间，从而避免了以前文献中提到的状态爆炸现象，同时该文用Needham-Schroeder公钥协议和TMN协议来说明如何应用该模型。     

一个支持软件需求验证的过程模型研究

需求验证是软件需求阶段的一个重要环节,未经验证的需求给项目成功带来较大的需求风险。在前期研究的基础上,从需求验证的基本原理和可操作性出发,提出一个支持需求验证的过程模型(RVPM),进行形式化描述,并论述了需求验证过程的几个关键过程和策略。结合实例,分析了如何应用该模型来指导需求验证过程。理论和实例分析表明：该模型有效地克服了需求验证过程的复杂性和经验操作,有效降低项目需求风险。     

Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting

Testing and Bounded Model Checking (BMC) are two techniques used in Software Verification for bug-hunting. They are expression of two different philosophies: testing is used on the compiled code and it is more suited to find errors in common behaviors, while BMC is used on the source code to find errors in uncommon behaviors of the system. Nowadays, testing is by far the most used technique for software verification in industry: it is easy to use and even when no error is found, it can release a set of tests certifying the (partial) correctness of the compiled system. In the case of safety critical software, in order to increase the confidence of the correctness of the compiled system, it is often required that the provided set of tests covers 100% of the code. This requirement, however, substantially increases the costs associated to the testing phase, since it often involves the manual generation of tests. In this paper we show how BMC can be productively applied to the Software Verification process in industry. In particular, we show how to productively use a Bounded Model Checker for C programs (CBMC) as an automatic test generator for the Coverage Analysis of Safety Critical Software. In particular, we experimented CBMC on a subset of the modules of the European Train Control System (ETCS) of the European Rail Traffic Management System (ERTMS) source code, an industrial system for the control of the traffic railway, provided by Ansaldo STS. The Code of the ERTMS/ETCS, with thousands of lines, has been used as trial application with CBMC obtaining a set of tests satisfying the target 100% code coverage, requested by the CENELEC EN50128 guidelines for software development of safety critical systems. The use of CBMC for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the costs of the testing phase. To the best of our knowledge, this is the first time that BMC techniques have been used in an industrial setting for automatically generating tests achieving full coverage of Safety-Critical Software. The positive results demonstrate the maturity of Bounded Model Checking techniques for automatic test generation in industry.     

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).     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。