Formal methods encompass a wide choice of techniques and tools for the specification, development, analysis, and verification of software and hardware systems. Formal methods are widely applied in industry, in activities ranging from the elicitation of requirements and the early design phases all the way to the deployment, configuration, and runtime monitoring of actual systems. Formal methods allow one to precisely specify the environment in which a system operates, the requirements and properties that the system should satisfy, the models of the system used during the various design steps, and the code embedded in the final implementation, as well as to express conformance relations between these specifications. We present a broad scope of successful applications of formal methods in industry, not limited to the well-known success stories from the safety-critical domain, like railways and other transportation systems, but also covering other areas such as lithography manufacturing and cloud security in e-commerce, to name but a few. We also report testimonies from a number of representatives from industry who, either directly or indirectly, use or have used formal methods in their industrial project endeavours. These persons are spread geographically, including Europe, Asia, North and South America, and the involved projects witness the large coverage of applications of formal methods, not limited to the safety-critical domain. We thus make a case for the importance of formal methods, and in particular of the capacity to abstract and mathematical reasoning that are taught as part of any formal methods course. These are fundamental Computer Science skills that graduates should profit from when working as computer scientists in industry, as confirmed by industry representatives.

Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.

This article revisits soundness and completeness of proof systems for proving that sets of states in infinite-state labeled transition systems satisfy formulas in the modal mu-calculus in order to develop proof techniques that permit the seamless inclusion of new features in this logic. Our approach relies on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used to reason about the sound and complete tableau method for this problem due to Bradfield and Stirling. We also show how the flexibility of our lattice-theoretic basis simplifies reasoning about tableau-based proof strategies for alternative classes of systems. In particular, we extend the modal mu-calculus with timed modalities, and prove that the resulting tableau method is sound and complete for timed transition systems.

This paper proposes the use of static analysis to improve the generation of invariants from test data extracted from Simulink models. Previous work has shown the utility of such automatically generated invariants as a means for updating and completing system specifications; they also are useful as a means of understanding model behavior. This work shows how the scalability and accuracy of the data mining process can be dramatically improved by using information from data/control flow analysis to reduce the search space of the invariant mining and to eliminate false positives. Comparative evaluations of the process show that the improvements significantly reduce execution time and memory consumption, thereby supporting the analysis of more complex models, while also improving the accuracy of the generated invariants.

In this paper, we survey recent progress in CyberCardia project, a CPS Frontier project funded by the National Science Foundation. The CyberCardia project will lead to significant advances in the state of the art for system verification and cardiac therapies based on the use of formal methods and closed-loop control and verification. The animating vision for the work is to enable the development of a true in silico design methodology for medical devices that can be used to speed the development of new devices and to provide greater assurance that their behavior matches designer intentions, and to pass regulatory muster more quickly so that they can be used on patients needing their care. The acceleration in medical-device innovation achievable as a result of the CyberCardia research will also have long-term and sustained societal benefits, as better diagnostic and therapeutic technologies enter into the practice of medicine more quickly.

Many systems make use of concurrent tasks, however it is often difficult to test concurrent design. Therefore, many test cases are simplified and do not fully test all concurrency aspects of the system. We encountered this problem when analyzing test cases for concurrent flight software at NASA. To address this problem, we developed and evaluated a model based testing (MBT) technique for testing of concurrent systems. Using MBT, the tester creates a model, which is based on the requirements of the system under test (SUT), and lets the computer generate innumerable test cases automatically from the model. We evaluate the effectiveness of the technique using Microsoft's Spec Explorer MBT tool. We apply the technique on NASA's Core Flight Software (cFS) software bus module API, which is based on a concurrent publisher-subscriber architecture style and is a safety-critical system. We describe how we created a test automation architecture for testing concurrent inter-task communication as carried out by the software bus. We also investigate the type of issues the technique for testing of concurrent systems can find as well as what degree of code coverage it can achieve.

New research is underway at the FDA to investigate the benefits of integrating architecture analysis into safety evaluations of medical-device software. Due to the complexity in setting up testing environments for such software, the FDA is unable to conduct large-scale safety testing, instead, it must rely on other techniques to build an argument for whether the software is safe or not. The architecture analysis approach, formalized using relational algebra, is based on reconstructing abstract, yet precise, architectural views from source code to help build such arguments about safety. This paper discusses the use of the formal approach to analyze the Computer-Assisted Resuscitation Algorithm (CARA) software, which controls an infusion pump designed to provide automated assistance for transfusing blood. The results suggest that a) architecture analysis offers many insights related to software quality in general and testability (i.e., the ease of testing) and its impact on safety in particular, and b) architectural analysis results can be used to help configure static analysis tools to improve their performance for verifying safety properties.

Software architecture has become essential in the struggle to manage today's increasingly large and complex systems. Software architecture views are created to capture important system characteristics on an abstract and, thus, comprehensible level. As the system is implemented and later maintained, it often deviates from the original design specification. Such deviations can have implication for the quality of the system, such as reliability, security, and maintainability. Software architecture compliance checking approaches, such as the reflexion model technique, have been proposed to address this issue by comparing the implementation to a model of the systems' architecture design. However, architecture compliance checking approaches focus solely on structural characteristics and ignore behavioral conformance. This is especially an issue in Systems-of-Systems. Systems-of-Systems (SoS) are decompositions of large systems, into smaller systems for the sake of flexibility. Deviations of the implementation to its behavioral design often reduce the reliability of the entire SoS. An approach is needed that supports the reasoning about behavioral conformance on architecture level.In order to address this issue, we have developed an approach for comparing the implementation of a SoS to an architecture model of its behavioral design. The approach follows the idea of reflexion models and adopts it to support the compliance checking of behaviors. In this paper, we focus on sequencing properties as they play an important role in many SoS. Sequencing deviations potentially have a severe impact on the SoS' correctness and qualities. The desired behavioral specification is defined in UML sequence diagram notation and behaviors are extracted from the SoS implementation. The behaviors are then mapped to the model of the desired behavior and the two are compared. Finally, a reflexion model is constructed that shows the deviations between behavioral design and implementation. This paper discusses the approach and shows how it can be applied to investigate reliability issues in SoS.

This paper discusses the results of an application of a formally based verification technique, called Instrumentation-Based Verification (IBV), to a production automotive lighting controller. The goal of the study is to assess, from both a tools as well as a methodological perspective, the performance of IBV in an industrial setting. The insights obtained as a result of the project include a refinement of a previously developed architecture for requirements specifications; observations about changes to model-based design workflows; insights into the role of requirements during development; and the capability of automated verification to detect inconsistencies among requirements as well as between requirements and design models.

This paper shows how an architecture description notation that has support for timed events can be used to provide a meta-language for specifying exact communication semantics. The advantages of such an approach is that a designer is made fully aware of the ramifications of her design choices so that an attacker can no longer take advantage of hidden assumptions

This paper introduces triggered message sequence charts (TMSCs), a graphical, mathematically well-founded framework for capturing scenario-based system requirements of distributed systems. Like message sequence charts (MSCs), TMSCs are graphical depictions of scenarios, or exchanges of messages between processes in a distributed system. Unlike MSCs, however, TMSCs are equipped with a notion of trigger that permits requirements to be made conditional, a notion of partiality indicating that a scenario may be subsequently extended, and a notion of refinement for assessing whether or not a more detailed specification correctly elaborates on a less detailed one. The TMSC notation also includes a collection of composition operators allowing structure to be introduced into scenario specifications so that interactions among different scenarios may be studied. In the first part of this paper, TMSCs are introduced and their use in support of requirements modeling is illustrated via two extended examples. The second part develops the mathematical underpinnings of the language

This paper develops a framework for solving temporal-logic query-checking problems for a class of infinite-state system models that compute with integer-valued variables (so-called Presburger systems, in which Presburger formulas are used to define system behavior). The temporal-logic query checking problem may be formulated as follows: given a model and a temporal logic formula with placeholders, compute a set of assignments of formulas to placeholders such that the resulting temporal formula is satisfied by the given model. Temporal-logic query checking has proved useful as a means for requirements and design understanding; existing work, however, has focused only on propositional temporal logic and finite-state systems.Our method is based on a symbolic model-checking technique that relies on proof search. The paper first introduces this model-checking approach and then shows how it can be adapted to solving the temporal queries in which formulas may contain integer variables. We also present experimental results showing the computational efficacy of our approach.

This paper presents a local algorithm for solving the universal parametric real-time model-checking problem. The problem may be phrased as follows: given a real-time system and temporal formula, both of which may contain parameters, and a constraint over the parameters, does every allowed parameter assignment ensure that the real-time system satisfies the formula? Our approach relies on translating these model-checking problems into predicate equation systems, and then using an efficient proof-search algorithm to solve these systems. Experimental data shows that our method substantially outperforms existing approaches for systems that contain errors, while exhibiting comparable behavior for systems that are correct. This fast error-detection capability of our technique makes it especially interesting for design approaches in which model checkers are used "early and often" to detect design errors in an ongoing manner.

This paper develops a modeling paradigm called Architectural Interaction Diagrams, or AIDs, for the high-level design of systems containing concurrent, interacting components. The novelty of AIDs is that they introduce interaction mechanisms, or buses, as first-class entities into the modeling vocabulary. Users then have the capability, in their modeling, of using buses whose behavior captures interaction at a higher level of abstraction than that afforded by modeling notations such as Message Sequence Charts or process algebra, which typically provide only one fixed interaction mechanism. This paper defines AIDs formally by giving them an operational semantics that describes how buses combine subsystem transitions into system-level transitions. This semantics enables AIDs to be simulated; to incorporate subsystems given in different modeling notations into a single system model; and to use testing, debugging and model checking early in the system design cycle in order to catch design errors before they are implemented.

Triggered message sequence charts (TMSCs) are a visual, mathematically precise notation for capturing system requirements as conditional and partial scenarios. We show how TMSCs may be used to formalize two different requirements modeling methodologies. The first approach combines prescriptive ("do this") and constraint-based ("don't do that") requirements within a single specification; it is useful for composing localized subsystem requirements with global system ones. The second approach supports layered specifications in which partial descriptions of requirements may be elaborated on in a succession of steps; it is suitable for the incremental development of complex behavior in which "error" scenarios are "layered on top of" normative ones. Both methodologies derive their formal robustness from the notion of semantic refinement for TMSCs, which is based on DeNicola's and Hennessy's must preorder. Case studies are used to illustrate the utility of the work.

We propose an extension to Message Sequence Charts called Triggered Message Sequence Charts (TMSCs) that are intended to capture system specifications involving nondeterminism in the form of conditional scenarios. The visual syntax of TMSCs closely resembles that of MSCs; the semantics allows us to translate a TMSC specification into a framework that supports a notion of refinement based on Denicola's and Hennessy's must preorder. A simple but non-trivial example illustrates the utility of our extension to MSCs.

The paper describes the application of an automated verification tool to a software model developed at Ford Motor Company. Ford already has in place an advanced model-based software development framework that employs the Matlab(R), Simulink(R), and Stateflow(R) modeling tools. During this project, we applied the invariant checker Salsa to a Simulink(R)/Stateflow(R) 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.

Statecharts is a visual language for specifying reactive system behavior. The formalism extends traditional finite-state machines with notions of hierarchy and concurrency, and it is used in many popular software design notations. A large part of the appeal of Statecharts derives from its basis in state machines, with their intuitive operational interpretation. The classical semantics of Statecharts, however, suffers from a serious defect; it is not compositional, meaning that the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation, and it also provides the necessary foundation for reusability.

This paper studies the use of an equational variant of the modal /spl mu/-calculus as a unified framework for efficient temporal logic model checking. In particular we show how an expressive temporal logic, CTL*, may be efficiently translated into the /spl mu/-calculus. Using this translation, one may then employ /spl mu/-calculus model-checking techniques, including on-the-fly procedures, BDD-based algorithms and compositional model-checking approaches, to determine if systems satisfy formulas in CTL*.

This paper presents a testing-based semantic theory for reasoning about the efficiency of concurrent systems as measured in terms of the amount of their internal activity. The semantic preorders are given an algebraic characterization, and their optimality is established by means of a full abstractness result. They are also shown to subsume existing bisimulation-based efficiency preorders. An example is provided to illustrate the utility of this approach.

This paper presents a testing-based semantic preorder that relates real-time systems given in the process description language TPL on the basis of the predictability of their timing behavior. This predictability is measured in terms of the amount of variability present in processes' "activity-completion times". The semantic preorder is shown to coincide with an already existing, well-investigated implementation relation for TPL-the must-preorder. The optimality of our relation is also established by means of a full abstraction result. An example is provided to illustrate the utility of this work.

This paper describes a modeling and verification environment for real-time systems. The environment supports both a graphical design language (Modechart) and a textually based one (Temporal CCS) and implements different methodologies, including simulation, system minimization, and equivalence checking, for analyzing systems. The tool has been applied to the verification of active structural control systems.

This paper gives an on-the-fly algorithm for determining whether a finite-state system satisfies a formula in the temporal logic CTL. The time complexity of our algorithm matches that of the best existing "global algorithm" for model checking in this logic, and it performs as well as the best known global algorithms for the sublogics CTL and LTL. In contrast with these approaches, however, our routine constructs the state space of the system under consideration in a need-driven fashion and will therefore perform better in practice.

This paper develops a semantic framework for concurrent languages with value passing. An operation analogous to substitution in the λ-calculus is given, and a semantics is given for a value-passing version of Milner's Calculus of Communicating Systems (CCS). An operational equivalence is then defined and shown to coincide with Milner's (early) bisimulation equivalence. We also show how semantics maybe given for languages with asynchronous communication primitives. In contrast with existing approaches to value passing, this semantics does not reduce data exchange to pure synchronization over (potentially infinite) families of ports indexed by data, and it avoids variable renamings that are not local to processes engaged in communication.

Describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it to be correct.>

The paper develops a generalized approach to schedulability analysis that is mathematically founded in a process algebra called RTSL. Within RTSL one may describe the functional behavior, timing behavior, timing constraints (or deadlines), and scheduling discipline for real-time systems. The formal semantics of RTSL then allows the reachable state space of finite state systems to be automatically generated and searched for timing exceptions. We provide a generalized schedulability analysis technique to perform this state-based analysis.>

Abstract In this paper we show how the testing equivalences and preorders on transition systems may be interpreted as instances of generalized bisimulation equivalences and prebisimulation preorders. The characterization relies on defining transformations on the transition systems in such a way that the testing relations on the original systems correspond to (pre)bisimulation relations on the altered systems. On the basis of these results, it is possible to use algorithms for determining the (pre)bisimulation relations in the case of finite-state transition systems to compute the testing relations.

The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.

A framework for generating testing preorders that relate processes on the basis of their timing behavior as well as their degree of relative nondeterminism is developed. The basic concepts of transition systems and testing are reviewed, and timed testing, which takes account of the delay exhibited by a process as it attempts to pass a test, is introduced. The framework is then applied to two different scenarios. In the first, relations are constructed that relate processes on the basis of all timing considerations. In the second, relations are constructed that relate processes on the basis of their relative speeds. In both cases, alternative denotational characterizations of the resulting preorders are presented, and examples are given to illustrate the utility of the approach.>

A technique is presented for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being specified enough, for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula, then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using the results, the authors develop compositional proof rules for establishing the correctness of networks of parallel processes and illustrate their use with several examples. >