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.     

Modalities for model checking: branching time logic strikes back

We consider automatic verification of finite state concurrent programs. The global state graph of such a program can be viewed as a finite (Kripke) structure, and amodel checking algorithm can be given for determining if a given structure is a model of a specification expressed in a propositional temporal logic. In this paper, we present a unified approach for efficient model checking under a broad class of generalized fairness constraints in a branching time framework extending that of Clarke et al. (1983). Our method applies to any type of fairness expressed in a certain canonical form. Almost all ‘practical’ types of fairness from the literature, including the fundamental notions of impartiality, weak fairness, and strong fairness, can be succintly written in our canonical form. Moreover, our branching time approach can easily be adapted to handle types of fairness (such as fair reachability of a predicate) which cannot even be expressed in a linear temporal logic. We go on to argue that branching time logic is always better than linear time logic for model checking. We show that given any model checking algorithm for any system of linear time logic (in particular, for the usual system of linear time logic) there is a model checking algorithm of the same order of complexity (in both the structure and formula size) for the corresponding full branching time logic which trivially subsumes the linear time logic in expressive power (in particular, for the system of full branching time logic CTL^*). We also consider an application of our work to the theory of finite automata on infinite strings.     

Consequence Verification of Flowcharts

A common basis is presented, for Floyd's method of inductive assertions and for the subgoal induction method of Morris and Wegbreit. This basis is provided by consequence verification, a method for verifying logic programs. We connect flowcharts with logic programs by giving a recursive definition of the set of all computations of a flowchart. This definition can be given in two ways: the recursion can run forward or backward. Both definitions can be expressed in logic, resulting in a logic program which is then subjected to consequence verification. Verification of the forward logic program is shown to be essentially Floyd's method; verification of the backward program corresponds similarly to subgoal induction.     

The OPIT system I. A file-handling scheme for data in large applications programs

The OPIT program is briefly described. OPIT is a basis-set-optimising, self-consistent field, molecular orbital program for calculating properties of closed shell ground states of atoms and molecules. A file handling technique is then put forward which enables core storage to be used efficiently in large FORTRAN scientific applications programs. Hashing and list processing techniques, of the type frequently used in writing system software and computer operating systems, are here applied to the creation of data files (integral label and value lists etc.). Files consist of a chained series of blocks which may exist in core or on backing store or both. Efficient use of core store is achieved and the processes of file deletion, file re-writing and garbage collection of unused blocks can be easily arranged. The scheme is exemplified with reference to the OPIT program.A subsequent paper will describe a job scheduling scheme for large programs of this sort.     

Program partition and logic program analysis

A program partition scheme for stratified programs introduced by Apt et al. (1988) is used to study efficient computation of logic programs. We consider three types of program partitions and their corresponding graph representations: 1) the natural partition, 2) stratified partitions, and 3) the reduced partition. The natural (program) partition consists of definitions of relations, each definition being a subprogram. Subprograms of a program partition may consist of several relations. A partition graph is introduced for a program partition, each node of which corresponds to a subprogram. The partition graph for a stratified partition is a directed acyclic graph (DAG). A stratified partition decomposes a program into modules. The stratified partition with the maximum number of modules is the reduced partition. The cost to achieve a reduced partition is linear in the program size, using well known graph algorithms. We introduce the modular interpretations, which are equivalent in semantics to the standard interpretation. The modular interpretations offer encapsulation and may reduce the computation cost for some modules significantly. The modular approach can play an important role in query optimization, efficient termination, programming design, and software engineering. We classify query types and answer types then discuss query optimization for some query types. Many efficient query processing strategies are applicable to restricted subclasses of programs. The program partition method allows us to select the most efficient strategy for each module. For example, if a module is a uniformly bounded recursion, then the module can be terminated efficiently. If a module defines the transitive closure, then efficient program transformations may be applied to this module     

Program equivalence checking by two-tape automata

This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If a dynamic frame is acyclic (i.e., all program statements are irreversible), then it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs in which the semantics of operators is determined by acyclic dynamic frames can be reduced to the emptiness problem for two-tape automata (compound machines).     

Solving logic program conflict through strong and weak forgettings

We consider how to forget a set of atoms in a logic program. Intuitively, when a set of atoms is forgotten from a logic program, all atoms in the set should be eliminated from this program in some way, and other atoms related to them in the program might also be affected. We define notions of strong and weak forgettings in logic programs to capture such intuition, reveal their close connections to the notion of forgetting in classical propositional theories, and provide a precise semantic characterization for them. Based on these notions, we then develop a general framework for conflict solving in logic programs. We investigate various semantic properties and features in relation to strong and weak forgettings and conflict solving in the proposed framework. We argue that many important conflict solving problems can be represented within this framework. In particular, we show that all major logic program update approaches can be transformed into our framework, under which each approach becomes a specific conflict solving case with certain constraints. We also study essential computational properties of strong and weak forgettings and conflict solving in the framework.     

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.     

Slicing Software for Model Construction

Applying finite-state verification techniques (e.g., model checking) to software requires that program source code be translated to a finite-state transition system that safely models program behavior. Automatically checking such a transition system for a correctness property is typically very costly, thus it is necessary to reduce the size of the transition system as much as possible. In fact, it is often the case that much of a program's source code is irrelevant for verifying a given correctness property.In this paper, we apply program slicing techniques to remove automatically such irrelevant code and thus reduce the size of the corresponding transition system models. We give a simple extension of the classical slicing definition, and prove its safety with respect to model checking of linear temporal logic (LTL) formulae. We discuss how this slicing strategy fits into a general methodology for deriving effective software models using abstraction-based program specialization.     

Checking security properties by model checking

A method is proposed for checking security properties in programs written in high‐level languages. The method is based on the model checking technique. The SMV tool is used. The representation of the program is a Kripke structure modelling the control flow graph enriched with security information. The properties considered are secure information flow and the absence of covert channels caused by program termination. The formulae expressing these security properties are given using the logic CTL. Copyright © 2003 John Wiley & Sons, Ltd.     

Program derivation in type theory: A partitioning problem

Martin-Löf's type theory is a theory in which one can write both specifications and programs. By interpreting propositions as types, predicate logic is available when formulating a specification. The rules of type theory are formulated as tactics which makes a “top down” construction of programs possible. These ideas are illustrated by a formal derivation of a program for a partitioning problem.     

Dependently typed array programs don’t go wrong

The array programming paradigm adopts multidimensional arrays as the fundamental data structures of computation. Array operations process entire arrays instead of just single elements. This makes array programs highly expressive and introduces data parallelism in a natural way. Array programming imposes non-trivial structural constraints on ranks, shapes, and element values of arrays. A prominent example where such constraints are violated are out-of-bound array accesses. Usually, such constraints are enforced by means of run time checks. Both the run time overhead inflicted by dynamic constraint checking and the uncertainty of proper program evaluation are undesirable.We propose a novel type system for array programs based on dependent types. Our type system makes dynamic constraint checks obsolete and guarantees orderly evaluation of well-typed programs. We employ integer vectors of statically unknown length to index array types. We also show how constraints on these vectors are resolved using a suitable reduction to integer scalars. Our presentation is based on a functional array calculus that captures the essence of the paradigm without the legacy and obfuscation of a fully-fledged array programming language.     

A pragmatic type concept for Prolog supporting polymorphism, subtyping, and meta-programming

Approaches to typing logic programs often exclude various features of Standard Prolog. The system “Typical for annotated Prolog” (TaP) is a pragmatic approach to type checking programs written in Prolog without restricting the scope of the language. TaP checks Prolog programs that are extended with type declarations that support parametric polymorphism and subtyping. The purpose of this paper is to present an approach that extends Typical by meta-types for handling Prolog meta-programming techniques.     

Automated test generation using model checking: an industrial evaluation

In software development, testers often focus on functional testing to validate implemented programs against their specifications. In safety-critical software development, testers are also required to show that tests exercise, or cover, the structure and logic of the implementation. To achieve different types of logic coverage, various program artifacts such as decisions and conditions are required to be exercised during testing. Use of model checking for structural test generation has been proposed by several researchers. The limited application to models used in practice and the state space explosion can, however, impact model checking and hence the process of deriving tests for logic coverage. Thus, there is a need to validate these approaches against relevant industrial systems such that more knowledge is built on how to efficiently use them in practice. In this paper, we present a tool-supported approach to handle software written in the Function Block Diagram language such that logic coverage criteria can be formalized and used by a model checker to automatically generate tests. To this end, we conducted a study based on industrial use-case scenarios from Bombardier Transportation AB, showing how our toolbox CompleteTest can be applied to generate tests in software systems used in the safety-critical domain. To evaluate the approach, we applied the toolbox to 157 programs and found that it is efficient in terms of time required to generate tests that satisfy logic coverage and scales well for most of the programs.     

Kima: An Automated Error Correction System for Concurrent Logic Programs

We have implemented Kima, an automated error correction system for concurrent logic programs. Kima corrects near-misses such as wrong variable occurrences in the absence of explicit declarations of program properties.Strong moding/typing and constraint-based analysis are turning out to play fundamental roles in debugging concurrent logic programs as well as in establishing the consistency of communication protocols and data types. Mode/type analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode/type constraints, and can be solved efficiently. We proposed a simple and efficient technique which, given a non-well-moded/typed program, diagnoses the reasons of inconsistency by finding minimal inconsistent subsets of mode/type constraints. Since each constraint keeps track of the symbol occurrence in the program, a minimal subset also tells possible sources of program errors.Kima realizes automated correction by replacing symbol occurrences around the possible sources and recalculating modes and types of the rewritten programs systematically. As long as bugs are near-misses, Kima proposes a rather small number of alternatives that include an intended program. Search space is kept small because the minimal subset confines possible sources of errors in advance. This paper presents the basic algorithm and various optimization techniques implemented in Kima, and then discusses its effectiveness based on quantitative experiments.     

Language-Based Program Verification via Expressive Types

Recent developments in the area of expressive types have the prospect to supply the ordinary programmer with a programming language rich enough to verify complex program properties. Program verification is made possible via tractable type checking. We explore this possibility by considering two specific examples; verifying sortedness and resource usage verification. We show that advanced type error diagnosis methods become essential to assist the user in case of type checking failure. Our results point out new research directions for the development of programming environments in which users can write and verify their programs.     

Regular model checking for LTL(MSO)

Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics monadic second-order logic (MSO) and LTL as a natural logic for expressing the temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a buchi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature.     

Low-cost,Concurrent Checking of Pointer and Array Accesses in C Programs

Illegal pointer and array accesses are a major cause of failure for C programs. We present a technique called ‘guarding’ to catch illegal array and pointer accesses. Our implementation of guarding for C programs works as a source-to-source translator. Auxiliary objects called guards are added to a user program to monitor pointer and array accesses at run time. Guards maintain attributes to catch out of bounds array accesses and accesses to deallocated memory. Our system has found a number of previously unreported errors in widely-used Unix utilities and SPEC92 benchmarks. Many commonly used programs have bugs which may not always manifest themselves as a program crash, but may instead produce a subtly wrong answer. These programs are not routinely checked for run-time errors because the increase in execution time due to run-time checking can be very high. We present two techniques to handle the high cost of run-time checking of pointer and array accesses in C programs: ‘customization’ and ‘shadow processing’. Customization works by decoupling run-time checking from original computation. A user program is customized for guarding by throwing away computation not relevant for guarding. We have explored using program slicing for customization. Customization can cut the overhead of guarding by up to half. Shadow processing uses idle processors in multiprocessor workstations to perform run-time checking in the background. A user program is instrumented to obtain a ‘main process’ and a ‘shadow process’. The main process performs computations from the orignal program, occasionally communicating a few key values to the shadow process. The shadow process follows the main process, checking pointer and array accesses. The overhead to the main process which the user sees is very low – almost always less than 10%. © 1997 by John Wiley & Sons, Ltd.