Symbolic model checking APSL

Property specification language (PSL) is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. In this paper, we present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be easily implemented via the BDD based symbolic approach. Moreover, we implement an extension of NuSMV, and this adapted version supports symbolic model checking of APSL. Experimental results show that this variant of PSL can be efficiently verified. Henceforth, symbolic model checking PSL can be carried out by a transformation from PSL to APSL and symbolic model checking APSL.     

Model checking large software specifications

In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in whether model checking can be effectively applied to large software specifications. To investigate this, we translated a portion of the state-based system requirements specification of Traffic Alert and Collision Avoidance System II (TCAS II) into input to a symbolic model checker (SMV). We successfully used the symbolic model checker to analyze a number of properties of the system. We report on our experiences, describing our approach to translating the specification to the SMV language, explaining our methods for achieving acceptable performance, and giving a summary of the properties analyzed. Based on our experiences, we discuss the possibility of using model checking to aid specification development by iteratively applying the technique early in the development cycle. We consider the paper to be a data point for optimism about the potential for more widespread application of model checking to software systems     

A symbolic manipulator for automated verification of reactive systems with heterogeneous data types

In this paper, we present the design and implementation of the Composite Symbolic Library, a symbolic manipulator for model checking systems with heterogeneous data types. Our tool provides a common interface for different symbolic representations, such as BDDs, for representing Boolean logic formulas and polyhedral representations for linear arithmetic formulas. Based on this common interface, these data structures are combined using a disjunctive composite representation. We propose several heuristics for efficient manipulation of this composite representation and present experimental results that demonstrate their performance. We used an object-oriented design to implement the Composite Symbolic Library. We imported the CUDD library (a BDD library) and the Omega Library (a linear arithmetic constraint manipulator that uses polyhedral representations) to our tool by writing wrappers around them which conform to our symbolic representation interface. Our tool supports polymorphic verification procedures which dynamically select symbolic representations based on the input specification. Our symbolic representation library can be used as an interface between different symbolic libraries, model checkers, and specification languages. We expect our tool to be useful in integrating different tools and techniques for symbolic model checking, and in comparing their performance.     

Formal semantics,modular specification,and symbolic verification of product-line behaviour

Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated algorithms, SPL model checking still faces the well-known state explosion problem. Moreover, there is a need for high-level specification languages usable in industry. We address the state explosion problem by applying the principles of symbolic model checking to FTS-based verification of SPLs. In order to specify properties on specific products only, we extend the temporal logic CTL with feature quantifiers. Next, we show how SPL behaviour can be specified with fSMV, a variant of SMV, the specification language of the industry-strength model checker NuSMV. fSMV is a feature-oriented extension of SMV originally introduced by Plath and Ryan. We prove that fSMV and FTSs are expressively equivalent. Finally, we connect these results to a NuSMV extension we developed for verifying SPLs against CTL properties.     

具有过去时态算子的计算树逻辑模型检测

在计算树逻辑(CTL)中引入过去时态算子,得到了表达力更强的属性规约语言CTLP,给出了CTLP 的模型检测算法及其固定点刻画.该算法的复杂性和CTL一样.固定点刻画使得CTLP的符号模型检测过程能够实现,从而有效克服了模型检测中的状态爆炸问题.     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

Verifying conformance of multi-agent commitment-based protocols

Although several approaches have been proposed to specify multi-agent commitment-based protocols that capture flexible and rich interactions among autonomous and heterogeneous agents, very few of them synthesize their formal specification and automatic verification in an integrated framework. In this paper, we present a new logic-based language to specify commitment-based protocols, which is derived from ACTL^1c, a logic extending CTL¹ with modalities to represent and reason about social commitments and their actions. We present a reduction technique that formally transforms the problem of model checking ACTL^1c to the problem of model checking GCTL¹ (an extension of CTL¹ with action formulae). We prove that the reduction technique is sound and we fully implement it on top of the CWB-NC model checker to automatically verify the NetBill protocol, a motivated and specified example in the proposed specification language. We also apply the proposed technique to check the compliance of another protocol: the Contract Net protocol with given properties and report and discuss the obtained results. We finally develop a new symbolic algorithm to perform model checking dedicated to the proposed logic.     

PSL空间关系扩展及其在企业建模中的应用

PSL是面向制造业信息集成的过程规范语言,用户可根据需求对其基本理论进行扩展。为了满足企业建模对空间关系的刻画需求,以空间关系RCC理论为基础,实现了PSL空间关系扩展。最后给出一个基于空间关系扩展的PSL应用实例。     

Embedding finite automata within regular expressions

Regular expressions and their extensions have become a major component of industry-oriented specification languages such as IEEE PSL [IEEE Standard for Property Specification Language (PSL). IEEE Std 1850™-2005]. The model checking procedure of regular expression based formulas, involves constructing an automaton which runs in parallel with the model.     

Fault localization using a model checker

If a program does not fulfill its specification, a model checker can deliver a counterexample. However, although such a counterexample shows how the specification can be violated, it typically comprises large parts of the program and gives little information about which of the visited statements is responsible for the error. In this article, we show that model checkers can also be used to perform model‐based diagnosis and thus fault localization. The approach leads to significantly more precise diagnoses than the state‐of‐the‐art and typically rules out 90–99% of the code as possible fault locations. The approach is general and can be applied to any system that is amenable to model checking (with respect to language and complexity). To demonstrate the applicability and high precision of our approach, we present implementations for C programs using two different model checking tools and show experimental results from the TCAS case study and an integration with the DDVerify framework to debug Linux device drivers. Copyright © 2009 John Wiley & Sons, Ltd.     

基于模拟关系的精化检测方法

精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同形式化语言进行建模,如能证明两者间存在某种精化关系且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质, traces、stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,大大提高了算法性能,且该方法能直接用于traces精化检测.在此基础上,本文提出了基于模拟关系的stable failures和failures-divergence精化检测方法.此外,本文还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.     

基于LSC的模型检验研究

LSC是一种表达能力很强的顺序图建模语言,模型检验技术是验证软件模型正确性的重要方法,提出了一个对LSC模型进行模型检验的方法,并实现了相关支持工具。首先分析了LSC语言,然后基于其语义提出了生成LSC等价状态模型的方法,进而对生成的状态模型进行模型检验;最后进行了实例研究,利用给出的实现工具检验了用CTL描述的验证性质。     

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.     

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.     

Using binary decision diagrams for representation and analysis of communication protocols

A symbolic representation of a state/transition system based on binary decision diagrams (BDDs) is generally more compact than an explicit representation like a state/transition table. This is due to regular and repetitive patterns occurring in state/transition systems. By exploiting this property, huge state spaces can be represented, and the resulting BDDs can be profitably used for activities such as symbolic model checking and sequential circuit synthesis. This paper shows how such techniques can be applied to communication protocols by presenting a systematic method to build BDD representations from protocol specifications expressed in the ISO standard protocol specification language LOTOS. The method exploits the compositionality of the process algebra of LOTOS to avoid the enumeration of all the states and transitions, takes also data into account, enables building the BDDs in the more convenient disjunctive partitioned form, and can handle any LOTOS specification characterized by a finite LTS. The method consists in partitioning the set of process definitions according to their mutual recursion relationships, building an LTS for each set of mutually recursive process definitions, encoding these LTSs as BDDs which in turn are combined together, according to the process algebraic operators, to obtain the overall BDD representation. An example is used throughout the paper to illustrate the method.     

多智能体系统时态认知规范高效符号模型检测的算法研究

Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法.     

Game-theoretic simulation checking tool

Model checking is one of the most commonly used methods for checking program correctness. In this method, one verifies a program model given by the Kripke structure (labeled transition system) rather than the program itself. The specification is usually given as a temporal logic formula. In many subtasks of model checking, it is necessary to use relations that are defined on the set of program models and preserve the satisfiability of temporal logic formulas. There exist many relations of this kind, which are called simulation relations. In the present paper, we introduce a tool designed to check a wide class of simulation relations between finite models of programs. This tool is based on the simulation checking game-theoretic approach. The tool consists of two components. The first component is the formal language, which allows one to define various simulation relations in terms of an antagonistic two-player game. The second component is a software tool that, given two labeled transition systems and simulation definition, is able to check whether this simulation is satisfied between these labeled transition systems.     

A top-down methodology for microprocessor validation

A major challenge in today's functional verification is the lack of a formal specification with which to compare the RTL model. We propose a novel top-down verification approach that allows specification of a design above the RTL. From this specification, it is possible to automatically generate assertion models and RTL reference models. We also demonstrate that symbolic simulation and equivalence checking can be applied to verify an RTL design against its specification.     

Model checking RAISE applicative specifications

Ensuring the correctness of a given software component has become a crucial aspect in software engineering and model checking provides an almost fully automatic way of achieving this goal. Due to the scalability problems of the model checking technique, it has become popular to apply it at early stages in the development process, when the size of the model is much smaller than the final code. Properties proved in this way can be shown to hold at the implementation level provided that the final code refines the original specification. In this paper we focus on the main issues for adding model checking functionality to the RAISE specification language (RSL) and present the semantic foundations of our current approach for doing so. We also describe a way to use model checking to verify RAISE confidence conditions, ensuring the soundness and completeness of the results checked in this way. We then present the most interesting details of the implementation of a tool that follows the described approach. Finally, we illustrate the application of the technique with two case studies: a Digital Multiplexed Radio Telephone System and the Mondex electronic purse.