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.

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.