Comparing model checking and logical reasoning for real-time systems

We apply both model checking and logical reasoning to a real-time protocol for mutual exclusion. To this end we employ PLC-Automata, an abstract notion of programs for real-time systems. A logic-based semantics in terms of Duration Calculus is used to verify the correctness of the protocol by logical reasoning. An alternative but consistent operational semantics in terms of Timed Automata is used to verify the correctness by model checkers. Since model checking of the full model does not terminate in all cases within an acceptable time we examine abstractions and their influence on model-checking performance. We present two abstraction methods that can be applied successfully for the protocol presented.Received June 1999Accepted in revised form September 2003 by M.R. Hansen and C. B. Jones     

Logic programs with abstract constraint atoms: The role of computations

We provide a new perspective on the semantics of logic programs with arbitrary abstract constraints. To this end, we introduce several notions of computation. We use the results of computations to specify answer sets of programs with constraints. We present the rationale behind the classes of computations we consider, and discuss the relationships among them. We also discuss the relationships among the corresponding concepts of answer sets. One of those concepts has several compelling characterizations and properties, and we propose it as the correct generalization of the answer-set semantics to the case of programs with arbitrary constraints. We show that several other notions of an answer set proposed in the literature for programs with constraints can be obtained within our framework as the results of appropriately selected classes of computations.     

Model-checking games for fixpoint logics with partial order models

In this paper, we introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the interleaving semantics of such models is not considered, some problems that may arise when using interleaving representations are avoided and new decidability results for partial order models of concurrency are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus, in a partial order setting they verify properties of a number of fixpoint modal logics that can specify, in concurrent systems with partial order semantics, several properties not expressible with the μ-calculus. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving, in terms of temporal expressive power, previous results in the literature.     

Refining Model Checking by Abstract Interpretation

Formal methods combining abstract interpretation and model-checking have been considered for automated analysis of software.In abstract model-checking, the semantics of an infinite transition system is abstracted to get a finite approximation on which temporal-logic/-calculus model-checking can be directly applied.The paper proposes two improvements of abstract model-checking which can be applied to infinite abstract transition systems:iA new combination of forwards and backwards abstract fixed-point model-checking computations for universal safety. It computes a more precise result than that computed by conjunction of the forward and backward analyses alone, without needing to refine the abstraction;When abstraction is unsound (as can happen in minimum/maximum path-length problems), it is proposed to use the partial results of a classical combination of forward and backward abstract interpretation analyses for universal safety in order to reduce, on-the-fly, the concrete state space to be searched by model-checking.     

Module Checking

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.     

Disjunctive LP+integrity constraints= stable model semantics

We show that stable models of logic programs may be viewed as minimal models of programs that satisfy certain additional constraints. To do so, we transform the normal programs into disjunctive logic programs and sets of integrity constraints. We show that the stable models of the normal program coincide with the minimal models of the disjunctive program thatsatisfy the integrity constraints. As a consequence, the stable model semantics can be characterized using theextended generalized closed world assumption for disjunctive logic programs. Using this result, we develop a bottomup algorithm for function-free logic programs to find all stable models of a normal program by computing the perfect models of a disjunctive stratified logic program and checking them for consistency with the integrity constraints. The integrity constraints provide a rationale as to why some normal logic programs have no stable models.     

Timing analysis of Ada tasking programs

Concurrent real-time software is increasingly used in safety-critical embedded systems. Assuring the quality of such software requires the rigor of formal methods. In order to analyze a program formally, we must first construct a mathematical model of its behavior. In this paper, we consider the problem of constructing such models for concurrent real-time software. In particular, we provide a method for building mathematical models of real-time Ada tasking programs that are accurate enough to verify interesting timing properties, and yet abstract enough to yield a tractable analysis on nontrivial programs. Our approach differs from schedulability analysis in that we do not assume that the software has a highly restricted structure (e.g. a set of periodic tasks). Also, unlike most abstract models of real-time systems, we account for essential properties of real implementations, such as resource constraints and run-time overhead     

Data-abstraction refinement: a game semantic approach

This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs with integer types. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its type system. We use a fully abstract game semantics in the style of Hyland and Ong and a more intensional version of the model that tracks nondeterminism introduced by abstraction in order to detect false counterexamples. These theoretical developments are incorporated in a new model-checking tool, Mage, which implements efficiently the data-abstraction refinement procedure using symbolic and on-the-fly techniques.     

Model checking for process rewrite systems and a class of action-based regular properties

We consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL.     

模糊交互时态逻辑的模型检测

交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题。首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性。然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析。     

A simplification of a real‐time verification problem

We revisit the problem of real‐time verification with dense‐time dynamics using timeout and calendar‐based models and simplify this to a finite state verification problem. We introduce a specification formalism for these models and capture their behaviour in terms of semantics of timed transition systems. We discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of a large fragment of these timeout and calender‐based transition systems into that on clock‐less finite state models through a two‐step process comprising of digitization and finitary reduction. This technique enables us to verify safety invariants for real‐time systems using finite state model checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction‐based proof methodology. In the same manner, we verify timeliness properties. Moreover, we can verify liveness for real‐time systems, which are not possible by using induction with infinite state model checkers. Copyright © 2016 John Wiley & Sons, Ltd.     

Model Checking Dynamic Memory Allocation in Operating Systems

Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state exploration, should be adapted to deal with this kind of structure. This paper presents a method to specify and verify properties of C programs with dynamic memory management. The proposal contains two main contributions. First, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The approach consists of defining a canonical representation of the heap, moving most of the information from the state vector to a global structure. We provide a formal semantics of the method that allows us to prove the soundness of the representation. Secondly, we combine temporal LTL and CTL logic to define a two-dimensional logic, in time and space, which is suitable to specify complex properties of programs with dynamic data structures. We also define the model checking algorithms for this logic. The whole method has been implemented in the well known model checker SPIN, and illustrated with an example where a typical memory reader/writer driver is modelled and analyzed.     

Model checking rational agents

Agent-oriented programming techniques seem appropriate for developing systems that operate in complex, dynamic, and unpredictable environments. We aim to address this requirement by developing model-checking techniques for the (automatic or semiautomatic) verification of rational-agent systems written in a logic-based agent-oriented programming language. Typically, developers apply model-checking techniques to abstract models of a system rather than the system implementation. Although this is important for detecting design errors at an early stage, developers might still introduce errors during coding. In contrast, developers can directly apply our model-checking techniques to systems implemented in an agent-oriented programming language, automatically verifying agent systems without the usual gap between design and implementation. We developed our techniques for AgentSpeak, a rational-agent programming language based on the AgentSpeak (L) abstract agent-oriented programming language. AgentSpeak shares many features of the agent-oriented programming paradigm. Similarly, we've developed techniques for automatically translating AgentSpeak programs into the model specification language of existing model-checking systems. In this way, we reduce the problem of verifying that an AgentSpeak system has certain BDI logic properties to a conventional LTL model-checking problem.     

Model driven code checking

Model checkers were originally developed to support the formal verification of high-level design models of distributed system designs. Over the years, they have become unmatched in precision and performance in this domain. Research in model checking has meanwhile moved towards methods that allow us to reason also about implementation level artifacts (e.g., software code) directly, instead of hand-crafted representations of those artifacts. This does not mean that there is no longer a place for the use of high-level models, but it does mean that such models are used in a different way today. In the approach that we describe here, high-level models are used to represent the environment for which the code is to be verified, but not the application itself. The code of the application is now executed as is by the model checker, while using powerful forms of abstraction on-the-fly to build the abstract state space that guides the verification process. This model-driven code checking method allows us to verify implementation level code efficiently for high-level safety and liveness properties. In this paper, we give an overview of the methodology that supports this new paradigm of code verification.     

基于Petri网的模型检测研究

模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.     

On the Construction of Monitors for Temporal Logic Properties

Temporal logic is a valuable tool for specifying correctness properties of reactive programs. With the advent of temporal logic model checkers, it has become an important aid for the verification of concurrent and reactive systems. In model checking the temporal logic properties are verified against models expressed in the tool's modelling language. In addition, model-checking techniques are useful to test actual implementations or to verify models of the system that are too detailed to be analysed by a model checker, by means of, for instance, simulation.A tableau construction is an algorithm that translates a temporal logic formula into a finite-state automaton that accepts precisely all the models of the formula. It is a key ingredient to checking satisfiability of a formula as well as to the automata-theoretic approach to model checking. An improvement to the efficiency of tableau constructions has been the development of on-the-fly versions.In this paper, we present a particular tableau construction for the incremental analysis of execution traces during test, simulation or model-checking. The automaton forms the basis of a monitor that detects both good and bad prefix of a particular kind, namely those that are informative for the property under investigation. We elaborate on the construction of the monitor and demonstrate its correctness.     

Symbolic execution with abstraction

We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously we proposed a combination of symbolic execution and model checking for the analysis of such programs: we put a bound on the size of the program inputs and/or the search depth of the model checker to limit the search state space. Here we look beyond bounded model checking and consider state matching techniques to limit the state space. We describe a method for examining whether a symbolic state that arises during symbolic execution is subsumed by another symbolic state. Since the number of symbolic states may be infinite, subsumption is not enough to ensure termination. Therefore, we also consider abstraction techniques for computing and storing abstract states during symbolic execution. Subsumption checking determines whether an abstract state is being revisited, in which case the model checker backtracks—this enables analysis of an under-approximation of the program behaviors. We illustrate the technique with abstractions for lists and arrays. We also discuss abstractions for more general data structures. The abstractions encode both the shape of the program heap and the constraints on numeric data. We have implemented the techniques in the Java PathFinder tool and we show their effectiveness on Java programs. This paper is an extended version of Anand et al. (Proceedings of SPIN, pp. 163–181, 2006).     

Heap-Bounded Assembly Language

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property, disallowing aliasing but allowing safe, in-place-update compilation of programming languages. We prove that HBAL is sound for a low-level untyped model of the machine, using a satisfiability relation that captures when a location correctly models a value of some type. This interpretation is closer to the machine than previous abstract machines used for typed assembly language models, and we separate typing of the store from an untyped operational semantics of programs, as would be required for proof-carrying code. Our ultimate aim is to design a family of assembly languages that have high-level typing features for expressing resource-bound constraints. We want to link the assembly-level with high-level languages expressing similar constraints, to provide end-to-end guarantees and a viable framework for proof-carrying code. HBAL is a first exemplifying step in this direction. It is designed as a target low-level language for Hofmann's LFPL language. Programs written in LFPL run in a bounded amount of heap space, and this property carries over when they are compiled to HBAL: the resulting program does not allocate store or assume an external garbage collector. Following LFPL, we include a special diamond resource type that stands for a unit of heap space of uncommitted type.