Recently, software practitioners, using model-based engineering and similar methods, have begun developing software from models. After creating a model of the required system behavior, a developer can obtain assurance of the model by validating that it captures the intended behavior and verifying that it satisfies critical properties. Invariants are important to both validation, as a check that the model's behavior matches the intended behavior, and verification, as auxiliaries in proving critical system properties, either automatically or with human guidance. A common approach to discovering invariants is to propose and then check candidate invariants. In contrast, our invariant generation techniques deduce invariants directly from the specification of a model. This paper presents more powerful versions of our earlier techniques for invariant generation and illustrates their utility for a real-world AirLock system.

Based on our recent experience in four projects, each focused on either security-critical or safety-critical software, this paper evaluates several notions, widely held by RE researchers, for their utility in practical software development. It describes four notions which in our view work in practice and five others which do not.

Building robust, secure distributed systems in the presence of transient faults, node failures, and changes in network topology poses a multitude of challenges. To meet current engineering challenges such as pervasive and ubiquitous computing, one must adopt model-driven approaches to build distributed applications. We propose the synchronous paradigm for component integration and coordination: developers use an abstraction that respects the synchrony hypothesis, i.e., each external event is processed by the system completely before the arrival of the next event. Based on the synchronous model, the Secure Operations Language (SOL) is designed as a verifiable language for the integration of high assurance systems.

Formal specifications of required system behavior can be analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior Transferring this confidence to the system implementation depends on a formal link between requirements and implementation. The automatic generation of probably correct code provides just such a link. While optimization is usually performed on code to achieve efficiency, we propose to optimize the formal specification before generating code, thus providing optimization independent of the particular code generation method. This paper investigates the use of invariants in optimizing code generated from formal specifications in the software cost reduction (SCR) tabular notation. We show that invariants (1) provide the basis for simplifying expressions that otherwise cannot be improved using traditional compiler optimization techniques, and (2) allow detection and elimination of parts of the specification that would lead to unreachable code.

This paper describes a compositional proof strategy for verifying properties of requirements specifications. The proof strategy, which may be applied using either a model checker or a theorem prover, uses known state invariants to prove state and transition invariants. Two proof rules are presented: a standard incremental proof rule analogous to Manna and Pnueli's incremental proof rule and a compositional proof rule. The advantage of applying the compositional rule is that it decomposes a large verification problem into smaller problems which often can be solved more efficiently than the larger problem. The steps needed to implement the compositional rule are described, and the results of applying the proof strategy to two examples, a simple cruise control system and a real-world Navy system, are presented. In the Navy example, compositional verification %based on the compositional proof using either theorem proving or model checking was three times faster than verification %model checking using based on the standard incremental (noncompositional) rule. In addition to the two above rules for proving invariants, a new compositional proof rule is presented for circular assume-guarantee proofs of invariants. While in principle the strategy and %the rules described for proving invariants may be applied to any state-based specification with parallel composition of components, the specifications in the paper are expressed in the SCR (Software Cost Reduction) tabular notation, the auxiliary invariants used in the proofs are automatically generated invariants, and the verification is supported by the SCR tools.

In earlier work (Jeffords and Heitmeyer, 1998) we developed a fixpoint algorithm for automatically generating state invariants, properties that hold in each reachable state of a state machine model, from state-based requirements specifications. Such invariants are useful both in validating requirements specifications and as auxiliary lemmas in proofs that a requirements specification satisfies other invariant properties. This paper describes a new related algorithm that strengthens state invariants generated by our initial algorithm and demonstrates the new algorithm on a simplified version of an automobile cruise control system. The paper concludes by describing how the two algorithms were used to generate state invariants from a requirements specification of a cryptographic device and how the invariants in conjunction with a theorem prover were used to prove formally that the device satisfies a set of critical security properties.

Automatic generation of state invariants, properties that hold in every reachable state of a state machine model, can be valuable in software development. Not only can such invariants be presented to system users for validation, in addition, they can be used as auxiliary assertions in proving other invariants. This paper describes an algorithm for the automatic generation of state invariants that, in contrast to most other such algorithms, which operate on programs, derives invariants from requirements specifications. Generating invariants from requirements specifications rather than programs has two advantages: 1) because requirements specifications, unlike programs, are at a high level of abstraction, generation of and analysis using such invariants is easier, and 2) using invariants to detect errors during the requirements phase is considerably more cost-effective than using invariants later in software development. To illustrate the algorithm, we use it to generate state invariants from requirements specifications of an automobile cruise control system and a simple control system for a nuclear plant. The invariants are derived from specifications expressed in the SCR (Software Cost Reduction) tabular notation.

This article describes a formal analysis technique, called consistency checking , for automatic detection of errors, such as type errors, nondeterminism, missing cases, and circular definitions, in requirements specifications. The technique is designed to analyze requirements specifications expressed in the SCR (Software Cost Reduction) tabular notation. As background, the SCR approach to specifying requirements is reviewed. To provide a formal semantics for the SCR notation and a foundation for consistency checking, a formal requirements model is introduced; the model represents a software system as a finite-state automation which produces externally visible outputs in response to changes in monitored environmental quantities. Results of two experiments are presented which evaluated the utility and scalability of our technique for consistency checking in real-world avionics application. The role of consistency checking during the requirements phase of software development is discussed.