NFM 2010

Accepted Papers

The program committee selected 20 regular papers and 4 short papers from over 50 submissions. Each paper was read by 4 reviewers.

Proceedings of the Second NASA Formal Methods Symposium appear as NASA Conference Publication NASA/CP-2010-216215, 2010. (BibTex)

Regular Papers

• Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene. Automatic Review of Abstract State Machines by Meta Property Verification (Talk, BibTex)

  A model review is a validation technique aiming to determine if a model not only fulfils the intended requirements, but also are of sufficient quality to be easy to develop, maintain, and enhance. The model review process is of extremely importance since it allows to identify defects early in the system development, reducing the cost of fixing them. Usually model review is performed by external qualified people, but there is nowadays an increasing desire to automatize this process by systematically checking formal specifications for known vulnerabilities or defects. In this paper we propose a technique to perform automatic review of Abstract State Machine formal specifications. We first detect a family of typical vulnerabilities and defects a developer can introduce during the modelling activity using the ASMs (or any other state-transition based formal approach) and we express such faults as the violation of meta-properties that guarantee certain quality attributes of the specification. These meta-properties are defined in terms of two logical operators Always and Sometime to capture properties that must be true in every state or eventually true in at least one state of the ASM under analysis. Then, we map the logical operators always and sometime to temporal logic formulas and we exploit the model checking facilities of AsmetaSMV, a model checker for ASM models based on NuSMV, to check the meta-property violation. The violation of a meta-property always means that the quality attribute is not met and indicates a potential fault in the model. As a proof of concept, we also report the result of applying this ASM review process to some benchmark specifications.

• Sylvie Boldo and Thi Minh Tuyen Nguyen. Hardware-independent Proofs of Numerical Programs (Talk, BibTex)

  On recent architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved.

• Andreas Bollin. Slice-based Formal Specification Measures - Mapping Coupling and Cohesion Measures to Formal Z (Talk, BibTex)

  This paper investigates whether existing slice-based measures can (reasonably) be mapped to the field of state-based specification languages. By making use of Z specifications this contribution renews the idea of slice-profiles and derives coupling and cohesion measures for them. These measures are then assessed by taking a critical look at their sensitiveness in respect to modifications on the specification source.

• Ricky Butler, George Hagen, Jeffrey Maddalon, César Muñoz, Anthony Narkawicz and Gilles Dowek. How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project (Talk, BibTex)

  In this paper we describe a process of algorithmic discovery that was driven by our goal of achieving complete, mechanically verified algorithms that compute conflict prevention bands for use in enroute air traffic management. The algorithms were originally defined in the PVS specification language and subsequently have been implemented in Java and C++. We do not present the proofs in this paper: instead, we describe the process of discovery and the key ideas that enabled the final formal proof of correctness.

• Nestor Cataño and Radu Siminiceanu. A Machine-Checked Proof of A State-Space Construction Algorithm (Talk, BibTex)

  This paper presents the correctness proof of Saturation, an algorithm for the state-space generation of concurrent systems, implemented at the core of the SMART tool. Unlike the Breadth First Search exploration algorithm, which is easy to understand and formalise, Saturation is a high-performance algorithm, employing a mutually-preemptive, doubly-recursive set of procedures that compute a series of non-trivial, nested local fixed points, corresponding to a chaotic global fixed point strategy. A pencil-and-paper proof of Saturation exists, but a machine checked proof has never been attempted. The key result of the proof is the characterisation theorem of saturated nodes in decision diagrams, stating that a saturated node represents a set of states encoding a local fixed-point with respect to firing all events affecting only the node's level and levels below. For our purpose, we have employed the Prototype Verification System (PVS) for formalising the Saturation algorithm, its data structures, and for conducting the proofs.

• Sagar Chaki and Arie Gurfinkel. Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications (Talk, BibTex)

  We develop a learning-based automated Assume-Guarantee (AG) reasoning framework for verifying omega-regular properties of concurrent systems. We study the applicability of non-circular (AG-NC) and circular (AG-C) AG proof rules in the context of systems with infinite behaviors. In particular, we show that AG-NC is incomplete when assumptions are restricted to strictly infinite behaviors, while AG-C remains complete. We present a general formalization, called LAG, of the learning based automated AG paradigm. We show how existing approaches for automated AG reasoning are special instances of LAG. We develop two learning algorithms for a class of systems, called regular systems, that combine finite and infinite behaviors. We show that for regular systems, both AG-NC and AG-C are sound and complete. Finally, we show how to instantiate LAG to do automated AG reasoning for regular, and omega-regular, systems using both AG-NC and AG-C as proof rules.

• Xiang Fu and Chung-Chih Li. Modeling Regular Replacement for String Constraint Solving (Talk, BibTex)

  Bugs in user input sanitation of software systems often lead to vulnerabilities. Among them many are caused by improper use of regular replacement. This paper presents a precise modeling of various semantics of regular substitution, such as the declarative, finite, greedy, and reluctant, using finite state transducers (FST). By projecting an FST to its input/output tapes, we are able to solve atomic string constraints, which can be applied to both the forward and backward image computation in model checking and symbolic execution of text processing programs. We report several interesting discoveries, e.g., certain fragments of the general problem can be handled using less expressive deterministic FST. A compact representation of FST is implemented in SUSHI, a string constraint solver. It is applied to detecting vulnerabilities in web applications.

• Xiaowan Huang, Anu Singh and Scott A. Smolka. Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol (Talk, BibTex)

  We use the Uppaal model checker for Timed Automata to verify the Timing-Sync time-synchronization protocol for sensor networks (TPSN). The TPSN protocol seeks to provide network-wide synchronization of the distributed clocks in a sensor network. Clock-synchronization algorithms for sensor networks such as TPSN must be able to perform arithmetic on clock values to calculate clock drift and network propagation delays. They must also be able to read the value of a local clock and assign it to another local clock. Such operations are not directly supported by the theory of Timed Automata. To overcome this formal-modeling obstacle, we augment the Uppaal specification language with the integer-clock derived type. Integer clocks, which are essentially integer variables that are periodically incremented by a global pulse generator, greatly facilitate the encoding of the operations required to synchronize clocks as in the TPSN protocol. With this integer-clock-based model of TPSN in hand, we use Uppaal to verify that the protocol achieves network-wide time synchronization and is devoid of deadlock. We also use the Uppaal Tracer tool to illustrate how integer clocks can be used to capture clock drift and resynchronization during protocol execution.

• Eduardo Rafael López Ruiz and Michel Lemoine. Can Regulatory Bodies Expect Efficient Help from Formal Methods? (Talk, BibTex)

  In the context of EDEMOI -a French national project that propounded the use of semi-formal and formal methods to infer the consistency and robustness of aeronautical regulations through the analysis of faithfully representative models- a methodology had been suggested (and applied) to different (safety and security-related) aeronautical regulations. This paper summarizes the preliminary results of this experience by stating: which were the methodology's expected benefits, from a scientific point of view, and which are its useful benefits, from a regulatory body's point of view.

• Srinivas Nedunuri, Douglas R. Smith and William R. Cook. Synthesis of Greedy Algorithms Using Dominance Relations (Talk, BibTex)

  Greedy algorithms exploit problem structure and constraints to achieve linear-time performance. Yet there is still no completely satisfactory way of constructing greedy algorithms. For example, the Greedy Algorithm of Edmonds depends upon translating a problem into an algebraic structure called a matroid, but the existence of such a translation can be as hard to determine as the existence of a greedy algorithm itself. An alternative characterization of greedy algorithms is in terms of dominance relations, a well-known algorithmic technique used to prune search spaces. We demonstrate a process by which dominance relations can be methodically derived for a number of greedy algorithms, including activity selection, and prefix-free codes. By incorporating our approach into an existing framework for algorithm synthesis, we demonstrate that it could be the basis for an effective engineering method for greedy algorithms. We also compare our approach with other ways of constructing greedy algorithms.

• Lehilton L. C. Pedrosa and Arnaldo V. Moura. A New Method for Incremental Testing of Finite State Machines (Talk, BibTex)

  The automatic generation of test cases is an important issue for conformance testing of several critical systems. We present a new method for the derivation of test suites when the specification is modeled as a combined Finite State Machine (FSM). A combined FSM is obtained conjoining previously tested submachines with newly added states. This new concept is used to describe a fault model suitable for incremental testing of new systems, or for retesting modified implementations. For this fault model, only the newly added or modified states need to be tested, thereby considerably reducing the size of the test suites. The new method is a generalization of the well-known W-method and the G-method, but is scalable, and so it can be used to test FSMs with an arbitrarily large number of states.

• Concetta Pilotto and Jerome White. Verification of Faulty Message Passing Systems with Continuous State Space in PVS (Talk, BibTex)

  We present a library of PVS meta-theories that verifies a class of distributed systems in which agents communicate via message-passing. The theoretic work consists of iterative schemes for solving systems of linear equations, such as message-passing extensions of the Gauss and Gauss-Seidel methods. We briefly review that work and discuss the challenges in formally verifying it.

• Petra Price and Greg Turgeon. Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking (Talk, BibTex)

  A feasibility study was performed on a representative aerospace system to determine the following: (1) the benefits and limitations to using SCADER, a commercially available tool for model checking, in comparison to using a proprietary tool that was studied previously [1] and (2) metrics for performing the model checking and for assessing the findings. This study was performed independently of the development task by a group unfamiliar with the system, providing a fresh, external perspective free from development bias.

• Dominic Richards and David Lester. A Prototype Embedding of Bluespec SystemVerilog in the PVS Theorem Prover (Talk, BibTex)

  Bluespec SystemVerilog (BSV) is a Hardware Description Language based on the guarded action model of concurrency. It has an elegant semantics, which makes it well suited for formal reasoning. However, little work has been done on applying mechanized verification to BSV designs. We present a prototype shallow embedding of BSV in the PVS higher order theorem prover. Our embedding is compatible with the PVS model checker, in order to reduce the effort of tedious proof components, leaving the verification engineer free to tackle the intellectually significant parts of a proof.

• Pritam Roy and Natarajan Shankar. SimCheck: An Expressive Type System for Simulink (Talk, BibTex)

  MATLAB Simulink is a member of a class of visual languages that are used for modeling and simulating physical and cyber-physical system. A Simulink model consists of blocks with input and output ports connected using links that carry signals. We extend the type system of Simulink with annotations and dimensions/units associated with ports and links. These types can capture invariants on signals as well as relations between signals. We define a typechecker that checks the well-formedness of Simulink blocks with respect to these type annotations. The type checker generates proof obligations that are solved by SRI's Yices solver for satisfiability modulo theories (SMT). This translation can be used to detect type errors, demonstrate counterexamples, generate test cases, or prove the absence of type errors. Our work is an initial step toward the symbolic analysis of MATLAB Simulink models.

• Matt Staats, Michael Whalen, Ajitha Rajan and Mats Heimdahl. Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness (Talk, BibTex)

  In black-box testing, the tester creates a set of tests to exercise a system under test without regard to the internal structure of the system. Generally, no objective metric is used to measure the adequacy of black-box tests. In recent work, we have proposed three requirements coverage metrics, allowing testers to objectively measure the adequacy of a black-box test suite with respect to a set of requirements formalized as Linear Temporal Logic (LTL) properties. In this report, we evaluate the effectiveness of these coverage metrics with respect to fault finding. Specifically, we conduct an empirical study to investigate two questions: (1) do test suites satisfying a requirements coverage metric provide better fault finding than randomly generated test suites of approximately the same size?, and (2) do test suites satisfying a more rigorous requirements coverage metric provide better fault finding than test suites satisfying a less rigorous requirements coverage metric? Our results indicate (1) that test suites satisfying more rigorous coverage metrics provide better fault finding than test suites satisfying less rigorous coverage metrics and (2) only one coverage metric proposed -- Unique First Cause (UFC) coverage -- is sufficiently rigorous to ensure test suites that perform better than random testing.

• Sarah Thompson, Guillaume Brat and Arnaud Venet. Software Model Checking of ARINC-653 Flight Code with MCP (BibTex)

  The ARINC-653 standard defines a common interface for Integrated Modular Avionics (IMA) code. In particular, ARINC-653 Part 1 specifies a process- and partition-management API that is analogous to POSIX threads, but with certain extensions and restrictions intended to support the implementation of high reliability flight code. MCP is a software model checker, developed at NASA Ames, that provides capabilities for model checking C and C++ source code. In this paper, we present recent work aimed at implementing extensions to MCP that support ARINC-653, and we discuss the challenges and opportunities that consequentially arise. Providing support for ARINC-653's time and space partitioning is nontrivial, though there are implicit benefits for partial order reduction possible as a consequence of the API's strict interprocess communication policy.

• Sanaz Yeganefard, Michael Butler and Abdolbaghi Rezazadeh. Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B (Talk, BibTex)

  Recently a set of guidelines, or cookbook, has been developed for modelling and refinement of control problems in Event-B. The Event-B formal method is used for system-level modelling by defining states of a system and events which act on these states. It also supports refinement of models. This cookbook is intended to systematise the process of modelling and refining a control problem system by distinguishing environment, controller and command phenomena. Our main objective in this paper is to investigate and evaluate the usefulness and effectiveness of this cookbook by following it throughout the formal modelling of cruise control system found in cars. The outcomes are identifying the benefits of the cookbook and also giving guidance to its future users.

• Xiang Yin and John Knight. Formal Verification of Large Software Systems (Talk, BibTex)

  We introduce a scalable proof structure to facilitate formal verification of large software systems. In our approach, we mechanically synthesize an abstract specification from the software implementation, match its static operational structure to that of the original specification, and organize the proof as the conjunction of a series of lemmas about the specification structure. By setting up a different lemma for each distinct element and proving each lemma independently, we obtain the important benefit that the proof scales easily for large systems. We present details of the approach and an illustration of its application on a challenge problem from the security domain.

• Yang Zhao and Gianfranco Ciardo. Symbolic Computation of Strongly Connected Components Using Saturation (Talk, BibTex)

  Finding strongly connected components (SCCs) in discrete-state models is a critical task in formal verification concerning LTL and fair CTL properties, but the potentially huge number of reachable states and SCCs constitutes a formidable challenge. This paper is devoted to computing the sets of states in SCCs and terminal SCCs in asynchronous systems. Motivated by its clear advantages in many applications, the idea of saturation is employed on two previously proposed approaches: Lockstep and transitive closure. First, saturation speeds up state-space exploration when computing each SCC in Lockstep. Then, our main contribution is a novel algorithm to compute the transitive closure using saturation. The experimental results indicate that our improved algorithms achieve a clear speedup over their original implementations. With the help of the new transitive closure computation algorithm, up to 10e+150 SCCs can be explored within a few seconds.

Short Papers

• Erik Endres, Christian Müller, Andrey Shadrin and Sergey Tverdyshev. Towards the Formal Verification of a Distributed Real-Time Automotive System (Talk, BibTex)

  We present the status of a project which aims at building, formally and pervasively verifying a distributed automotive system. The target system is a gate-level model which consists of several interconnected electronic control units with independent clocks. This model is verified against the specification as seen by an operating system programmer. The automotive system is implemented on several FPGA boards. The pervasive verification is carried out using combination of interactive theorem proving (Isabelle/HOL) and model checking (LTL).

• Viet Yen Nguyen, Thomas Noll and Max Odenbrett. Slicing AADL Specifications for Model Checking (Talk, BibTex)

  To combat the state-space explosion problem in model checking larger systems, abstraction techniques can be employed. Here, methods that operate on the system specification before constructing its state space are preferable to those that try to minimize the resulting transition system as they generally reduce peak memory requirements. In this paper we sketch a slicing algorithm for system specifications written in (a variant of) the Architecture Analysis and Design Language (AADL). Given a system specification and a property to be verified, it automatically removes those parts of the specification that are irrelevant for model checking the property, thus reducing the size of the corresponding transition system. The applicability and effectiveness of our approach is demonstrated by analyzing the state-space reduction for some examples, employing a translator from AADL to Promela, the input language of the SPIN model checker.

• Pierre Roux and Radu Siminiceanu. Model Checking with Edge-valued Decision Diagrams (Talk, BibTex)

  We describe an algebra of Edge-Valued Decision Diagrams (EVMDDs) to encode arithmetic functions and its implementation. We provide efficient algorithms for manipulating EVMDDs and give upper bounds of the theoretical time complexity of these algorithms for all basic arithmetic and relational operators. We also demonstrate that the time complexity of the generic recursive algorithm for applying a binary operator on EVMDDs is no worse than that of Multi-Terminal Decision Diagrams. We have implemented a new symbolic model checker with the intention to represent in one formalism the best techniques available at the moment across a spectrum of existing tools: EVMDDs for encoding arithmetic expressions, identity-reduced MDDs for representing the transition relation, and the saturation algorithm for reachability analysis. We compare our new symbolic model checking EVMDD library with the widely used CUDD package and show that, in many cases, our tool is several orders of magnitude faster than CUDD.

• Christian Saad and Bernhard Bauer. Data-flow Based Model Analysis (Talk, BibTex)

  The concept of (meta) modeling combines an intuitive way of formalizing the structure of an application domain with a high expressiveness that makes it suitable for a wide variety of use cases and has therefore become an integral part of many areas in computer science. While the definition of modeling languages through the use of meta models, e.g. in UML, is a well-understood process, their validation and the extraction of behavioral information is still a challenge. In this paper we present a novel approach for dynamic model analysis along with several fields of application. Examining the propagation of information along the edges and nodes of the model graph allows to extend and simplify the definition of semantic constraints in comparison to the capabilities offered by e.g. the Object Constraint Language. Performing a flow-based analysis also enables the simulation of dynamic behavior, thus providing an abstract interpretation-like analysis method for the modeling domain.