Reactis is a commercially successful testing and validation tool which is implemented almost entirely in Standard ML. Our experience using a functional language to develop a commercial product has led us to the conclusion that while functional languages have some disadvantages, in the case of Reactis the benefits of a functional language substantially outweigh the drawbacks.

Reactive Systems, Inc. (RSI) was founded in 1999 with the goal of developing and marketing tools that help engineers improve software quality while decreasing software development costs. RSI launched its Reactis testing and validation package in 2002 and has subsequently built a customer base that includes over 30 major automotive and aerospace companies located around the world. In this presentation, we discuss how the use of Standard ML (SML) has proved to be a key factor in the success of RSI. The use of SML as the primary implementation language for Reactis has yielded substantial productivity improvements that enabled a small team to develop, deploy, enhance and maintain a very complex product. In addition to its use in Reactis, RSI leverages SML to build the company intranet (which automates a number of important business processes), to build its public website, and to implement an extensive automated regression test suite for Reactis. We will also describe some more intangible benefits such as the role that pervasive SML use has played in attracting and retaining highly productive employees.

This paper discusses the concept of Instrumentation-Based Validation (IBV): the use of model instrumentation and coverage-based testing to validate models of embedded control software. IBV proceeds as follows. An engineer first formalizes requirements as assertions, or small models, which may be thought of as monitors that observe the behavior of the controller model as it executes. The engineer then instruments the model with these assertions and develops test suites with the aim of highlighting where assertion violations occur. To make our discussion of IBV more concrete, we also consider its implementation within the Reactis tool suite for the automated testing and validation of controller models given in ® /Stateflow®.

Despite the enormous strides made in automatic verification technology over the past decade and a half, tools such as model checkers remain relatively underused in the development of software. One reason for this is that the bewildering array of specification and verification formalisms complicates the development and adoption by users of relevant tool support. This paper proposes a remedy to this state of affairs in the case of finite-state concurrent systems by describing an approach to developing customizable yet efficient verification tools.

This paper describes the application of an automated verification tool to a software model developed at Ford. Ford already has in place an advanced model-based software development framework that employs the MATLAB, Simulink, and Stateflow modeling tools. During this project we applied the invariant checker Salsa to a Simulink / Stateflow model of automotive software to check for nondeterminism, missing cases, dead code, and redundant code. During the analysis, a number of anomalies were detected that had not been found during manual review. We argue that the detection and correction of these problems demonstrates a cost-effective application of formal verification that elevates our level of confidence in the model.

Salsa is an invariant checker for specifications in SAL (the SCR Abstract Language). To establish a formula as an invariant without any user guidance, Salsa carries out an induction proof that utilizes tightly integrated decision procedures for discharging the verification conditions. Currently, Salsa requires the invariants to be inductive and implements a combination of BDD algorithms and a constraint solver for integer linear arithmetic. The user interface of Salsa is designed to mimic the widely popular interface of model checkers; i.e., given a formula and a system description either establish their consistency (but return no proof) or provide a counterexample in case of failure. In either case, the algorithm must terminate. Unlike model checkers, however, Salsa returns a state pair as a counterexample and not an execution sequence. Also, since an invariant is required to be inductive, users must validate the counterexamples. The use of induction enables Salsa to combat the state explosion problem that plagues model checkers - it can handle specifications whose state spaces are too large for model checkers to analyze. Also, unlike general purpose theorem provers, Salsa concentrates on a single task and gains efficiency by employing specifically optimized heuristics.

We present TwoTowers, a tool for analyzing functional and performance properties of concurrent systems expressed as terms in the stochastically timed reward process algebra EMPAr. TwoTowers builds on two existing tools, CWB-NC and MarCA, that have been retargeted to carry out functional and performance analysis (respectively) of EMPAr system specifications. As an example, we describe the application of TwoTowers to the Lehmann-Rabin randomized distributed algorithm for the dining philosopher problem.

Although a number of mechanical provers have been introduced and applied widely by academic researchers, these provers are rarely used in the practical development of software. For mechanical provers to be used more widely in practice, two major barriers must be overcome. First, the languages provided by the mechanical provers for expressing the required system behavior must be more natural for software developers. Second, the reasoning steps supported by mechanical provers are usually at too low and detailed a level and therefore discourage use of the prover. To help remove these barriers, we are developing a system called TAME, a high-level user interface to PVS for specifying and proving properties of automata models. TAME provides both a standard specification format for automata models and numerous high-level proof steps appropriate for reasoning about automata models. In previous work, we have shown how TAME can be useful in proving properties about systems described as Lynch-Vaandrager Timed Automata models. TAME has the potential to be used as a PVS interface for other specification methods that are specialized to define automata models. This paper first describes recent improvements to TAME, and then presents our initial results in using TAME to provide theorem proving support for the SCR (Software Cost Reduction) requirements method, a method with a wide range of other mechanized support.

Despite the enormous strides made in automatic verification technology over the past decade and a half, tools such as model checkers remain relatively underused in the development of software. One reason for this is that the bewildering array of specification and verification formalisms complicates the development and adoption by users of relevant tool support. This paper proposes a remedy to this state of affairs in the case of finite-state concurrent systems by describing an approach to developing customizable yet efficient verification tools.

This dissertation presents a customizable tool framework for the automatic verification of concurrent systems. We identify several fundamental concepts that serve as the building blocks for the extensible tool framework realized in the Concurrency Workbench of North Carolina (CWB-NC) and the Process Algebra Compiler of North Carolina (PAC-NC). The CWB-NC supports a variety of different types of verification and may be easily extended to support new ones. The PAC-NC eases the task of changing the design language supported by the CWB-NC. Given a high-level description of the syntax and semantics of a language, the PAC-NC generates the code necessary to retarget the CWB-NC to the new language. The semantic component of a PAC-NC language description is based on structural operational semantics (SOS) an intuitive yet formal approach to defining the semantics of languages. In order for our framework to be applicable to real-world concurrent systems, which are typically very complex and very big, the code generated by the PAC-NC must be extremely efficient in both time and space. We have therefore focused considerable attention on optimizing PAC-generated code. The PAC-NC has been used to generate CWB-NC front ends for a number of different design languages. The utility of the customizable approach was investigated by applying it to a case study that examined part of a network in a railway signaling system.

The NCSU Concurrency Workbench is a tool for verifying finite-state systems. A key feature is its flexibility; its modular design eases the task of adding new analyses and changing the language users employ for describing systems. This note gives an overview of the system's features, including its capacity for generating diagnostic information for incorrect systems, and discusses some of its applications.

This paper illustrates the use of priorities in process algebras by a real-world example dealing with the design of a safety-critical network which is part of a railway signaling system. Priorities in process algebras support an intuitive modeling of distributed systems since undesired interleavings can be suppressed. This fact also leads to a substantial reduction of the sizes of the models. We have implemented a CCS-based process algebra with priorities as a new front-end for the NCSU Concurrency Workbench, and we used model checking for verifying properties of the signaling system.

This paper describes the Process Algebra Compiler (PAC), a front-end generator for process-algebra-based verification tools. Given descriptions of a process algebra's concrete and abstract syntax and semantics as structural operational rules, the PAC produces syntactic routines and functions for computing the semantics of programs in the algebra. Using this tool greatly simplifies the task of adapting verification tools to the analysis of systems described in different languages; it may therefore be used to achieve source-level compatibility between different verification tools. Although the initial verification tools targeted by the PAC are MAUTO and the Concurrency Workbench, the structure of the PAC caters for the support of other tools as well.