Abstract The SCOOP model extends the Eiffel programming language to provide support for concurrent programming. The model is based on the principles of Design by Contract. The semantics of contracts used in the original proposal (SCOOP_97) is not suitable for concurrent programming because it restricts parallelism and complicates reasoning about program correctness. This article outlines a new contract semantics which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that it is indeed a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs—similar to those for traditional non-concurrent programs—of partial correctness and loop termination in the presence of asynchrony.

Abstract SCOOP is a concurrent programming language with a new semantics for contracts that applies equally well in concurrent and sequential contexts. SCOOP eliminates race conditions and atomicity violations by construction. However, it is still vulnerable to deadlocks. In this paper we describe how far contracts can take us in verifying interesting properties of concurrent systems using modular Hoare rules and show how theorem proving methods developed for sequential Eiffel can be extended to the concurrent case. However, some safety and liveness properties depend upon the environment and cannot be proved using the Hoare rules. To deal with such system properties, we outline a SCOOP Virtual Machine (SVM) as a fair transition system. The SVM makes it feasible to use model-checking and theorem proving methods for checking global temporal logic properties of SCOOP programs. The SVM uses the Hoare rules where applicable to reduce the number of steps in a computation.

Model-driven development, using languages such as UML and BON, often makes use of multiple diagrams (e.g., class and sequence diagrams) when modeling systems. These diagrams, presenting different views of a system of interest, may be inconsistent. A metamodel provides a unifying framework in which to ensure and check consistency, while at the same time providing the means to distinguish between valid and invalid models, that is, conformance. Two formal specifications of the metamodel for an object-oriented modeling language are presented, and it is shown how to use these specifications for model conformance and multiview consistency checking. Comparisons are made in terms of completeness and the level of automation each provide for checking multiview consistency and model conformance. The lessons learned from applying formal techniques to the problems of metamodeling, model conformance, and multiview consistency checking are summarized.

Abstract. We present a refinement calculus for transforming object-oriented (OO) specifications (or ‘contracts’) of classes into executable Eiffel programs. The calculus includes the usual collection of algorithmic refinement rules for assignments, if-statements, and loops. However, the calculus also deals with some of the specific challenges of OO, namely rules for introducing feature calls and reference types (involving aliasing). The refinement process is compositional in the sense that a class specification is refined to code based only on the specifications (not the implementations) of the classes that the specification depends upon. We discuss how automated support for such a process can be developed based on existing tools. This work is done in the context of a larger project involving methods for the seamless design of OO software in the graphical design notation BON (akin to UML). The goal is to maintain model and source code integrity, i.e., the software developer can work on either the model or the code, where (ideally) changes in one view are reflected instantaneously and automatically in all views.

We contrast modelling languages that are founded on the use of a single model with those founded on use of multiple models. We propose that to best support the seamless and reversible development of reliable software, languages that follow the single-model principle are superior. We define this principle precisely, and discuss when it is insufficient, particularly for early requirements engineering.

Reactive systems exhibit ongoing, possibly nonterminating, interaction with the environment. Real-time systems are reactive systems that must satisfy quantitative timing constraints. This paper presents a structured compositional design method for discrete real-time systems that can be used to combat the combinatorial explosion of states in the verification of large systems. A composition rule describes how the correctness of the system can be determined from the correctness of its modules, without knowledge of their internal structure. The advantage of compositional verification is clear. Each module is both simpler and smaller than the system itself. Composition requires the use of both model-checking and deductive techniques. A refinement rule guarantees that specifications of high-level modules are preserved by their implementations. The StateTime toolset is used to automate parts of compositional designs using a combination of model-checking and simulation. The design method is illustrated using a reactor shutdown system that cannot be verified using the StateTime toolset (due to the combinatorial explosion of states) without compositional reasoning. The reactor example also illustrates the use of the refinement rule.

The article shows how to make a transition from the Z formal notation to the Business Object Notation (BON). It is demonstrated that BON has the expressive power of Z, with the additional advantages of object-orientation and a supporting seamless development method. The transition is illustrated for some widely used Z constructs. The translation lays the groundwork for a semi-automated tool for extracting classes from Z specifications.

Real-time distributed systems are modeled by a times transition model (TTM). For any finite-state TTM, decision procedures are provided for checking a small but important class of properties (specified in real-time temporal logic). The procedures are linear in the size of the system reachability graph. The class of properties includes invariance, precedence, eventuality and real-time response specifications.>

Decision procedures are presented for checking a small but useful class of properties for any finite-state system consisting of real-time discrete-event processes. A timed transition model (TTM) is used for representing real-time discrete-event processes, and real-time temporal logic (RTTL) is the assertion language in which the property to be verified is stated. The relationship of TTMs to other formalisms is summarized along with a complete definition of TTMs and an overview of RTTL. The construction of reachability graphs is discussed, two different procedures are presented for constructing reachability graphs, and the corresponding decision procedures are given.>

Real-time systems are modeled by a timed transition model (TTM). For any finite-state TTM, decision procedures are provided for checking a small but important class of properties, which are specified in real-time temporal logic. The procedures are linear in the size of the system reachability graph. The class of properties includes invariance, precedence, eventuality, and real-time response specifications.>