Slicing communicating automata specifications: polynomial algorithms for model reduction

In the industry, communicating automata specifications are mainly used in fields where the reliability requirements are high, as this formalism allow the use of powerful validation tools. Still, on large scale industrial specifications, formal methods suffer from the combinatorial explosion phenomenon. In our contribution, we suggest to try to bypass this phenomenon, in applying slicing techniques preliminarily to the targeted complex analysis. This analysis can thus be performed a posteriori on a reduced (or sliced) specification, which is potentially less exposed to combinatorial explosion. The slicing method is based on dependence relations, defined on the specification under analysis, and is mainly founded on the literature on compiler construction and program slicing. A theoretical framework is described, for static analyses of communicating automata specifications. This includes formal definitions for the aforementioned dependence relations, and for a slice of a specification with respect to a slicing criterion. Efficient algorithms are also described in detail, for calculating dependence relations and specification slices. Each of these algorithms has been shown to be polynomial, and sound and complete with respect to its respective definition. These algorithms have also been implemented in a slicing tool, named Carver, that has shown to be operational in specification debugging and understanding. The experimental results obtained in model reduction with this tool are promising, notably in the area of formal validation and verification methods, e.g.model checking, test case generation.     

The KeY tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.     

A comparison of tools for teaching formal software verification

We compare four tools regarding their suitability for teaching formal software verification, namely the Frege Program Prover, the Key system, Perfect Developer, and the Prototype Verification System (PVS). We evaluate them on a suite of small programs, which are typical of courses dealing with Hoare-style verification, weakest preconditions, or dynamic logic. Finally we report our experiences with using Perfect Developer in class.     

Design verification in model-based?��-controller development using an abstract component

Component-based software development is a promising approach for controlling the complexity and quality of software systems. Nevertheless, recent advances in quality control techniques do not seem to keep up with the growing complexity of embedded software; embedded systems often consist of dozens to hundreds of software/hardware components that exhibit complex interaction behavior. Unanticipated quality defects in a component can be a major source of system failure. To address this issue, this paper suggests a design verification approach integrated into the model-driven, component-based development methodology Marmot. The notion of abstract components—the basic building blocks of Marmot—helps to lift the level of abstraction, facilitates high-level reuse, and reduces verification complexity by localizing verification problems between abstract components before refinement and after refinement. This enables the identification of unanticipated design errors in the early stages of development. This work introduces the Marmot methodology, presents a design verification approach in Marmot, and demonstrates its application on the development of a μ-controller-based abstraction of a car mirror control system. An application on TinyOS shows that the approach helps to reuse models as well as their verification results in the development process.     

Verification of clocked and hybrid systems

This paper presents a new computational model for real-time systems, called the clocked transition system (CTS) model. The CTS model is a development of our previous timed transition model, where some of the changes are inspired by the model of timed automata. The new model leads to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety a nd liveness properties of clocked transition systems. All rules are associated with verification diagrams. The verification of response properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for u ntimed reactive systems, for proving all interesting properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTS isnon-zeno. Finally, we present an extension of the model and the invariance proof rule for hybrid systems. Received: 23 September 1998 / 7 June 1999     

Software model checking without source code

We present a framework, called air, for verifying safety properties of assembly language programs via software model checking. air extends the applicability of predicate abstraction and counterexample guided abstraction refinement to the automated verification of low-level software. By working at the assembly level, air allows verification of programs for which source code is unavailable—such as legacy and COTS software—and programs that use features—such as pointers, structures, and object-orientation—that are problematic for source-level software verification tools. In addition, air makes no assumptions about the underlying compiler technology. We have implemented a prototype of air and present encouraging results on several non-trivial examples.     

Automatic analysis of DMA races using model checking and <Emphasis Type="Italic">k</Emphasis>-induction

Modern multicore processors, such as the Cell Broadband Engine, achieve high performance by equipping accelerator cores with small “scratch-pad” memories. The price for increased performance is higher programming complexity – the programmer must manually orchestrate data movement using direct memory access (DMA) operations. Programming using asynchronous DMA operations is error-prone, and DMA races can lead to nondeterministic bugs which are hard to reproduce and fix. We present a method for DMA race analysis in C programs. Our method works by automatically instrumenting a program with assertions modeling the semantics of a memory flow controller. The instrumented program can then be analyzed using state-of-the-art software model checkers. We show that bounded model checking is effective for detecting DMA races in buggy programs. To enable automatic verification of the correctness of instrumented programs, we present a new formulation of k-induction geared towards software, as a proof rule operating on loops. Our techniques are implemented as a tool, Scratch, which we apply to a large set of programs supplied with the IBM Cell SDK, in which we discover a previously unknown bug. Our experimental results indicate that our k-induction method performs extremely well on this problem class. To our knowledge, this marks both the first application of k-induction to software verification, and the first example of software model checking in the context of heterogeneous multicore processors.     

Hybrid Verifications of Reactive Programs

We present in this paper some new language features and constructs, that allow the joint synchronous/asynchronous programming of reactive applications, as well as their formal verification. We show that reactive applications may be dealt with from two points of view. First, from the chronological point of view, i.e., when reactions are instantaneous, generated by event occurrences in discrete time. Second, from the chronometrical point of view, when reactions have durations in dense time. This duality must be expressible in languages that allow a consistent programming of both synchronous and asynchronous features. The objective of mixing these dual approaches leads to model reactive systems by using hybrid systems, to deal simultaneously with both discrete and continuous phenomena. Furthermore, this must be followed by some verification of the application's properties, with respect to its behavioural and quantitative features. We analyze several existing frameworks that meet these requirements, and propose our own approach based on the language Electre. Received December 1997 / Accepted in revised form September 1999     

Introductory paper: scalability aspects of validation

This special section is devoted to a selection of papers that appeared originally in the Proceedings of TACAS 2001, the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems [1] which took place in Genova, Italy in April 2001 as a constituent event of the European joint conferences on theory and Practice of Software. All papers present approaches, tools and algorithms that aim at extending the scope of formal techniques (coverage of systems specifications, data structures, size, and their trade-offs) for validation, verification, and testing of software systems. They are by no means a complete account of the numerous ways in which real software and software systems may become subject to rigorous investigation, but they provide an interesting sampling of novel approaches towards scalability of formal methods-based validation.     

Testing Formal Specifications to Detect Design Errors

Formal specification and verification techniques are now apused to increase the reliability of software systems. However, these proaches sometimes result in specifying systems that cannot be realized or that are not usable. This paper demonstrates why it is necessary to test specifications early in the software life cycle to guarantee a system that meets its critical requirements and that also provides the desired functionality. Definitions to provide the framework for classifying the validity of a functional requirement with respect to a formal specification tion are also introduced. Finally, the design of two tools for testing formal specifications is discussed.     

A WSDL-based type system for asynchronous WS-BPEL processes

We tackle the problem of providing rigorous formal foundations to current software engineering technologies for web services, and especially to WSDL and WS-BPEL, two of the most used XML-based standard languages for web services. We focus on a simplified fragment of WS-BPEL sufficiently expressive to model asynchronous interactions among web services in a network context. We present this language as a process calculus-like formalism, that we call ws-calculus, for which we define an operational semantics and a type system. The semantics provides a precise operational model of programs, while the type system forces a clean programming discipline for integrating collaborating services. We prove that the operational semantics of ws-calculus and the type system are ‘sound’ and apply our approach to some illustrative examples. We expect that our formal development can be used to make the relationship between WS-BPEL programs and the associated WSDL documents precise and to support verification of their conformance.     

Functional programming languages for verification tools: a comparison of Standard ML and Haskell

We compare Haskell with Standard ML as programming languages for verification tools based on our experience developing the verification platform Truth in Haskell and the Edinburgh Concurrency Workbench (CWB) in Standard ML. We review not only technical language features but also the worlds of the languages, for example, the availability of compilers, tools, and libraries. We also discuss the merits and difficulties of comparing programming languages in this wide sense and support our view that Truth and the CWB are similar enough to justify the conclusions drawn in this paper.     

Efficient debugging in a formal verification environment

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and design modification. Published online: 21 February 2003     

Reducing the size of resolution proofs in linear time

DPLL-based SAT solvers progress by implicitly applying binary resolution. The resolution proofs that they generate are used, after the SAT solver’s run has terminated, for various purposes. Most notable uses in formal verification are: extracting an unsatisfiable core, extracting an interpolant, and detecting clauses that can be reused in an incremental satisfiability setting (the latter uses the proof only implicitly, during the run of the SAT solver). Making the resolution proof smaller can benefit all of these goals: it can lead to smaller cores, smaller interpolants, and smaller clauses that are propagated to the next SAT instance in an incremental setting. We suggest two methods that are linear in the size of the proof for doing so. Our first technique, called Recycle-Units uses each learned constant (unit clause) (x) for simplifying resolution steps in which x was the pivot, prior to when it was learned. Our second technique, called   simplifies proofs in which there are several nodes in the resolution graph, one of which dominates the others, that correspond to the same pivot. Our experiments with industrial instances show that these simplifications reduce the core by ≈5% and the proof by ≈13%. It reduces the core less than competing methods such as run- till- fix, but whereas our algorithms are linear in the size of the proof, the latter and other competing techniques are all exponential as they are based on SAT runs. If we consider the size of the proof (the resolution graph) as being polynomial in the number of variables (it is not necessarily the case in general), this gives our method an exponential time reduction comparing to existing tools for small core extraction. Our experiments show that this result is evident in practice more so for the second method: rarely it takes more than a few seconds, even when competing tools time out, and hence it can be used as a cheap proof post-processing procedure.     

Graphical scenarios for specifying temporal properties: an automated approach

Temporal logics are commonly used for reasoning about concurrent systems. Model checkers and other finite-state verification techniques allow for automated checking of system model compliance to given temporal properties. These properties are typically specified as linear-time formulae in temporal logics. Unfortunately, the level of inherent sophistication required by these formalisms too often represents an impediment to move these techniques from “research theory” to “industry practice”. The objective of this work is to facilitate the nontrivial and error prone task of specifying, correctly and without expertise in temporal logic, temporal properties. In order to understand the basis of a simple but expressive formalism for specifying temporal properties we critically analyze commonly used in practice visual notations. Then we present a scenario-based visual language called Property Sequence Chart (PSC) that, in our opinion, fixes the highlighted lacks of these notations by extending a subset of UML 2.0 Interaction Sequence Diagrams. We also provide PSC with both denotational and operational semantics. The operational semantics is obtained via translation into Büchi automata and the translation algorithm is implemented as a plugin of our Charmy tool. Expressiveness of PSC has been validated with respect to well known property specification patterns. Preliminary results appeared in (Autili et al. 2006a).     

Before and after vacuity

In formal verification, we verify that a system is correct with respect to a specification. Cases like antecedent failure can make a successful pass of the verification procedure meaningless. Vacuity detection can signal such “meaningless” passes of the specification, and indeed vacuity checks are now a standard component in many commercial model checkers. We address two dimensions of vacuity: the computational effort and the information that is given to the user. As for the first dimension, we present several preliminary vacuity checks that can be done without the design itself, which implies that some information can be found with a significantly smaller effort. As for the second dimension, we present algorithms for deriving two types of information that are not provided by standard vacuity checks, assuming for a model M and formula φ: (a) behaviors that are possibly missing from M (or wrongly restricted by the environment) (b) the largest subset of occurrences of literals in φ that can be replaced with false simultaneously without falsifying φ in M. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors. A preliminary version of this article was published in the proceedings of MEMOCODE 2007 [18].