Amsterdam, The Netherlands, 14 - 17 May 2003



Farhad Arbab

Abstract Behavior Types : a Model for Components and Their Composition

The notion of Abstract Data Type (ADT) has served as a foundation model for structured and object-oriented programming for some thirty years. An ADT defines an algebra of operations with well-defined semantics, without specifying any detail about the implementation of those operations or the data structures they operate on to realize them. ADT is a powerful abstraction and encapsulation mechanism that groups data together with their related operations into logically coherent and loosely-dependent entities, such as objects, yielding better structured programs.

The current trend in software engineering toward component based systems requires a foundation model as well. We introduce the notion of an Abstract Behavior Type (ABT) as a higher-level alternative to ADT and propose it as a proper foundation model for both components and their composition. An ABT defines an abstract behavior as a relation among a set of timed-data-streams, without specifying any detail about the operations that may be used to implement such behavior or the data types it may manipulate for its realization. The ABT model supports much looser coupling than is possible with ADT and is inherently amenable to exogenous coordination. We propose that both of these are highly desirable, if not essential, properties for components and their composition.

In our view, a component based system consists of component instances and their connectors (i.e., the "glue code"), both of which are uniformly modeled as ABTs. As a concrete instance of the application of the ABT model, we present Reo: a channel-based exogenous coordination model wherein complex coordinators, called "connectors'' are compositionally built out of simpler ones. The simplest connectors in Reo are a set of channels with well-defined behavior supplied by users. Reo can be used as a "glue language'' for compositional construction of connectors that orchestrate component instances in a component-based system. We demonstrate the surprisingly expressive power of connector composition in Reo through a number of examples. Because all Reo connectors are ABTs, we show how the semantics of channel composition in Reo can be defined in terms of a calculus of ABT composition.

Jos Baeten

Another look at the the axiomatization of parallel composition

Different alternatives are investigated for the axiomatization of parallel composition in the presence of the explicit termination constant epsilon (skip). Emphasis is put on the completeness (ground equations are derivable exactly when they hold in the transition system model) and omega-completeness (same for open equations) of the different axiomatizations.

Michel Bidoit

On the Integration of Observability and Reachability Concepts

(note: based on joint work with Rolf Hennicker)

This talk focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. We develop the essential notions that are needed to construct an institution which takes into account both the generation- and observation-oriented aspects of software systems. Thereby the underlying paradigm is that the semantics of a specification should be as loose as possible to capture all its
correct realizations. We also consider the so-called "idealized models'' of a specification which are useful to study the behavioral properties a user can observe when he/she is experimenting with the system. Finally, we present sound and complete proof systems that allow us to derive behavioral properties from the axioms of a given specification.

Related Paper :
Michel Bidoit and Rolf Hennicker. Constructor-based Observational Logic.

Ed Brinksma (University of Twente)

Components, Performance and Compositionality - A Process Algebraic Approach

Philippe Darondeau

Automatic specifications of transition systems

(note: based on joint work with Eric Badouel)

Path-automatic specifications are rational presentations of sets of finite or infinite graphs. A specification is made of a regular set of paths and rational relations on this set. Each action is specified by two relations that define respectively when it may, or must occur. Two other relations tell which pairs of paths may, or must be confluent. We show that it is decidable whether some model of path-automatic specifications may be realized by some Petri net with transitions in bijection with the specified actions.

Willem-Paul de Roever

Verification for Java's monitor and multi-threading concepts

(note: based on joint work with Erika Abraham-Mumm (Albert-Ludwigs-University Freiburg), Frank S. de Boer (CWI Amsterdam), and Martin Steffen (Christian-Albrechts-University Kiel))

Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread-classes, allowing for a mutli-threaded flow of control. The concurrency model includes shared-variable concurrency via instace variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation.

To reason about safety-properties of multithreaded programs, we introduce in this paper an assertional proof-method for Java-MT
("Multi-Threaded Java"), a small concurrent sublanguage of Java covering the mentioned concurrency issues as well as the object-based
core of Java, i.e., object-creation, side effects, and aliasing, but leaves aside inheritance and subtyping. Proofs of soundness and
relative completeness of the proof method have been given.

E Allen Emerson

The States of Verification

We discuss the state(s) of formal verification. We claim that state-based model-theoretic methods (e.g., model checking) are more effective than proof-based approaches, despite state explosion. We argue that abstractions for systems comprised of many similar subcomponents are especially important in limiting state explosion. Economies of scale ensure that such replicated systems are common in practice.

(Replicated systems are also common in nature: the universe is understood to be comprised of many protons, neutrons, and electrons.) We describe efficient techniques for verifying various classes of replicated systems, including many classical synchronization problems, resource allocation problems, and cache coherence protocols. Some of the technical work described was done jointly with Kedar Namjoshi and Vineet Kahlon. Finally, we discuss how Moore's law can be expected to make model checking and related methods increasingly effective over time.

Process-Oriented, Consistent Integration of Software Components

Gregor Engels, Sebastian Thöne - University of Paderborn

The integration of software components and in particular the integration of elementary web services to larger-scale services has become an important issue in software engineering. Following a process-oriented approach, the compositions can be described as control and data flow between available web services or components. The compositions have to be integrated in a consistent way, i.e., their export interfaces have to be respected by their importing components. The talk discussed the Business Process Execution Language for Web Services (BPEL4WS), an existing service composition language, and proposed UML-WSC as an alternative, visual language extension of UML. For the advanced description of service interfaces, UML-WSC extends the type system of the established Web Service Definition Language (WSDL).

Links / Literature

R.Depke, G.Engels, M.Langham, B.Lütkemeier, and S.Thöne : Process-Oriented, Consistent Integration of Software Components In Proc. COMPSAC 2002, Oxford, UK, August 2002.IEEE, 2002.

S.Thöne, R.Depke, and G.Engels : Process-Oriented, Flexible Composition of Web Services with UML In Proc. of Joint Workshop on Conceptual Modeling Approaches for e-Business (eCOMO 2002); Tampere, Finland; Oct 2002, LNCS (to appear)

Maurizio Gabbrielli

Semantics and expressive power of shared dataspace languages

(note: based on joint work with N. Busi, F. de Boer, M.C. Meo and G. Zavattaro)

By using a suitable process calculus we formalize in a uniform setting several languages based on the shared dataspace model, including Linda, Gamma, Concurrent Constraint Programming (ccp) and their timed extensions. For these languages we define a semantics based on reactive sequences which for timed ccp is proven to be fully abstract w.r.t. the input/output notion of observable. We then compare the expressive power of these languages by using two different approaches: the first one, which allows to prove stronger encodability results, is based onthe notion of modular embedding while the second, which allow stronger separation results, uses a property preserving encoding of RAM in the target language. We show several encodability and separation results for shared dataspace languages and we sketch an application of these techniques to the case of pi-calculus.

Model-Based Design and Verification of Embedded Systems

Scalable formal analysis of embedded reactive programs demands the development of reasoning principles and algorithmic techniques that exploit the modular program structure. For architectural hierarchy that describes the communication structure between component processes, modular reasoning principles such as abstraction, compositional refinement, and assume-guarantee reasoning are well
understood and have been shown to be useful. In this talk we discuss the theory of modular reasoning for behavior hierarchy that describes control structure using hierarchic modes. First, we introduce the hierarchic reactive modules language that retains powerful features such as nested modes, mode reuse, exceptions, group transitions, history, and conjunctive modes, and yet has a semantic notion of mode hierarchy. We present an observational trace semantics for modes that provides the basis for mode refinement. We show the refinement
to be compositional with respect to the mode constructors, and develop an assume-guarantee reasoning principle. Then, we identify a variety of heuristics to exploit these modular features during reachability analysis. We report on an enumerative as well as a symbolic checker, and case studies.

Software Model Checking for Aspects and Superimpositions

(note: based on joint work with Marcelo Sihman)

Aspects and superimpositions describe augmentations to systems that cross-cut the usual division to objects or processes, yet can be
separately described, in a parametric way that encourages reuse. Examples treat monitoring, overflow, termination detection, and
many other concerns. The model checking of applications of aspects is explained, by showing the stages and proof obligations when a collection of generic aspects (called a superimposition) is combined with a basic program. We assume that both the basic program and the collection of aspects have their own specifications, where the superimposition specification describes assumptions about
underlying systems to which the superimposition may be applied, and the new functionality added by the superimposition. The Bandera
tool for Java programs is used to generate input for model checkers, although any similar tool could be employed. New
"verification aspects" and superimpositions are defined to modularize the proofs, and separate the proof-related augmentations to the code needed to apply Bandera from the basic program and the application aspects. This allows generating and activating
a series of model checking tasks automatically each time a superimposition is applied to a basic program, achieving
superimposition validation. A case study for a superimposition that monitors and checks an underlying bounded buffer program is

Configuration Theories and Their Application to Java

Configuration structures are a well-established true concurrency model for parallel computations. Configuration theories provide a logic for
a sub-class of configuration structures. Configurations are interpreted as partial computations represented as partial orders of events. Configuration theory axioms specify in which ways existing partial computations can be extended and composed into legal partial computations. We present a short introduction into configuration theories and the main soundness and completeness results. As an application we consider the formalisation of the Java memory model with configuration theories. The Java memory model can be axiomatised using simple configuration theory clauses directly representing the specification of the Java language. Since the current Java memory model is subject to change, we also consider some of the proposed changes that lead to a simplified and relaxed memory model. We again employ configuration theories to discuss these modifications.

Recent results on verification of concurrent systems using net unfoldings

This talk will outline a general technique for truncating Petri net unfoldings, parameterized according to the level of information about the original unfolding one wants to preserve. A key aspect of the proposed approach is an algorithm-independent notion of cut-off events, used to truncate a Petri net unfolding. Such a notion results in the unique canonical prefix of the unfolding. Canonical prefixes are complete and the talk will outline necessary and sufficient conditions for their finiteness. A surprising result is that after suitable generalization, the standard unfolding algorithm, and the parallel unfolding algorithm, despite being non-deterministic, generate the
canonical prefix.

Definitive Semantic Descriptions

Different programming languages often have a substantial number of constructs in common. For instance, most languages include arithmetic expressions; imperative languages generally include also assignment statements, statement sequences, conditional and iterative statements, variable declarations, and procedure declarations and calls; object-oriented languages include attributes and methods, and usually class declarations; and concurrent languages normally include some communication and synchronization primitives. Minor differences in the intended interpretation of "a" construct between languages can be dealt with by considering it as a family of related but distinct constructs, each having a well-defined (although possibly parametrized) intended interpretation.

A description of an individual construct can be regarded as _definitive_when it can be given once-and-for-all, and subsequently used _verbatim_ in the description of any language which includes that construct. In a framework supporting definitive descriptions, the semantic description of a complete programming language would consist merely of (instantiations of) the definitive descriptions of its individual constructs. The potential benefits of definitive semantic descriptions for applications of semantics are rather obvious; in particular, the thought of never having to write (or read!) more than one description of any construct seems quite appealing.

Monads in denotational semantics, categories of labels in modular SOS, and action notation in action semantics all provide a high degree of modularity when describing complete languages---but how close do they come to supporting definitive semantic descriptions of individual constructs ? and what kind of properties could be proved about individual constructs on the basis of their definitive descriptions? This talk addresses such questions, with the focus on modular SOS, which does indeed appear to support definitive operational descriptions.

A recent paper on MSOS.

Markus Müller-Olm

(Linear) Algebra for Program Analysis


Ernst-Rüdiger Olderog

Design of Real-Time Systems Implemented on PLCs

We present an approach to the design of correct real-time software for Programmable Logic Controllers (PLCs), a widespread hardware
platform in the area of traffic and automation control.

Requirements are formulated in a graphical formalism called Constraint Diagrams (CDs) developed by C. Kleuker. A CD consists of waveforms that describe the time-wise behaviour of observables and of arrows that describe the timed interdependencies between these waveforms. Design specifications are formulated as so-called PLC-Automata proposed by H. Dierks. These can be understood as a special class of timed automata that model in an abstract way the cyclic behaviour of PLCs. Programs are formulated in ST (Structured Text), a dedicated programming language for PLCs. PLC-Automata can be easily compiled into ST code. Alternatively, a compilation into C++ code executable on LEGO Mindstorm robots is possible.

The semantic link between CDs and PLC-Automata is stated in terms of the Duration Calculus, a logic and calculus for specifying real-time
behaviour due to Zhou, Hoare and Ravn. Using this semantics results on expressiveness of CDs and synthesis of PLC-Automata from subsets of CDs can be proven. To achieve an automatic verification of additional properties an alternative, equivalent semantics for PLC-Automata and CDs in terms of Timed Automata is defined. Then the model-checker UPPAAL can be used to establish these properties.

The approach is supported by a tool called Moby/PLC.

Wojciech Penczek

VERICS: A Tool for Verifying Timed Automata and Estelle Specifications

We present a new tool for automated verification of Timed Automata as well as protocols written in the specification language Estelle.
The current version offers an automatic translation from Estelle specifications to timed automata, and two complementary methods of
reachability analysis. The first one is based on Bounded Model Checking (BMC), while the second one is an on-the-fly verification on an abstract (pseudo-bisimilar) model of the system.

Erik Poll

Some thoughts on Java program specification and verification

In the LOOP project at the University of Nijmegen we are working on formal verification of sequential Java programs. More in particular, we look at programs that have been annotated using the specification language JML, and as case studies we have been looking at real industrial examples of Java Card programs for smart cards.

The aim of this talk is to give an overview of the achievements of the project so far, and to discuss the main challenges that we face in trying to scale up to larger Java(Card) programs, especially it comes to the use of class invariants and the use of references (aka pointers) in Java programs.

Anders P. Ravn

(joint work with Thomas Bak and Jan Dimon Bendtsen (Aalborg University)

Hybrid Control of a Mobile Robot - checking the path for safety

In the paper [BBR03], we present a hybrid systems solution to the problem of trajectory tracking for a four-wheel steered four-wheel driven mobile robot. The robot is modelled as a non-holonomic dynamic system subject to pure rolling, no-slip constraints. Under normal driving conditions, a nonlinear trajectory tracking feedback control law based on dynamic feedback linearization is sufficient to stabilize the system and ensure asymptotically stable tracking. Transitions to other modes are derived systematically from this model, whenever the configuration space of the controlled system has some fundamental singular points. The stability of the hybrid control scheme is finally analyzed using Lyapunov-like arguments.

The paper indicates, how to introduce a stability checking automaton that refines the control states of the controlling hybrid automata.. The refinement includes a new substate, unstable, which is entered when a constant rate overapproximation of the Lyapunov functions has not decreased sufficiently before exit conditions for the superstate are enabled and invariants ceases to hold.

The talk discussed, how superimposition of the stability checker on the control automaton gives a stability checker. This automaton may either be used as a simulator for offline checking of trajectories generated by a path planner or online. When used offline, the unstable state will reject the planned trajectory, when used online, reaching the unstable state may be accepted by locally relaxing the reference, e.g. relaxing constraints on velocity, because the local instability may thus be contained, such that id does not influence global stability.

It seems feasible to include the technique in an automated procedure in a tool like STATEFLOW.

[BBR03] Thomas Bak, Jan D. Bendtsen and Anders P. Ravn. Hybrid Control Design for a Wheeled Mobile Robot
In Hybrid Systems: Computation and Control (HSCC 2003) (Eds.: O. Maler and A. Pnueli), LNCS 2623, pp. 50-65, April 2003.

Jan Rutten

Modelling component connectors in Reo by constraint automata

(note: based on joint work with Farhad Arbab, Christel Baier and Marjan Sirjani)

A coinductive model for the component connector calculus Reo was presented in terms of relations (defined as greatest
fixed points) on timed data streams. In this talk, an operational counterpart of this stream model is presented, based on what we have called constraint automata.In these automata, transitions are labelled by name sets (indicating which ends of a channel or connector are simultaneously active), and have a constraint (on the input and output data of the active ends) as a value. The issues of product and hiding
of constraint automata, euivalence, and minimisation, will be briefly discussed.

In an earlier report :
F. Arbab, J.J.M.M. Rutten
A coinductive calculus of component connectors. Technical Report SEN-R0216, CWI, Amsterdam, 2002, pp. 1--17. To appear in the proceedings of WADT 2002. (Available at

Vladimiro Sassone

Deriving bisimulation congruences from first principles

G-relative pushouts (GRPOs) have recently been proposed as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. The talk explores the theory of GRPOs, arguing that they provide a simple and powerful basis towards a
comprehensive solution. As an example, we construct GRPOs in a category of `bunches and wirings' and we explain how to recast the approaches based on Milner's precategories and Leifer's functorial reactive systems into the 2-categorical theory of GRPOs.

Wolfram Schulte

The ABCs of Specification and Test: AsmL, Behavior, and Components

Wolfram Schulte, Microsoft Research, Redmond

This talk introduces AsmL and the AsmL tester. AsmL, an executable specification language, allows users to provide behavioral interfaces for components. This allows clients to fully understand the meaning of an implementation without access to the source code. AsmL uses behavioral subtyping to ensure the substitutability of components. In addition it provides many advanced specification features such as generic
types, transactional semantics, invariants and history constraints. The AsmL tester provides a tool-suite to check that a proposed implementation is a behavioral subtype of the specification. The toolset addresses stateless as well as stateful systems. It allows testing sequential as well as distributed systems. A demo of the tool set concludes the talk.

Igor Walukiewicz

Distributed games

A system consist of a process, of an environment and of possible ways of interaction between them. The synthesis problem is: given a specification \phi find a program P for the process such that the overall behaviour of the system satisfies \phi no matter what the bahaviour of the environment is.
One of the motivations for development of automata theory was the interest in verifying and synthesizing switching circuits. A circuit can be modeled as a function transforming infinite sequence of inputs into an infinite sequence of outputs. Church in 1963 has posed the problem of synthesizing such a function for a specification given in S1S, the monadic second order logic of one successor. The solution to this problem was given by Buchi and Ladweber in 1969. Nowadays we understand that this problem, and many other variations of the synthesis problem, reduce to finding a winning strategy in a two player game with perfect information and regular winning conditions.
A distributed system consist of some number of processes, each interacting in some way with the environment and other processes. The distributed synthesis problem is to find a program for each of the processes so that the global behaviour satisfies the given specification no matter what the behaviour of the environment is.
There are numerous ways of describing a distributed system and hence there are numerous ways of formalizing the distributed synthesis
problem. One way, suggested by Pnueli and Rosner, is to consider a system as an architecture: a graph of communication channels connecting boxes into which we need to put I/O programs. The other way, introduced by Rudie and Wonham, is to specify the sets of controllable and observable actions for each of the components of the system. For these and other settings there are algorithms solving the distributed synthesis problem for some cases.
In the distributed synthesis we do not understand very well what makes the problem decidable or undecidable. Each decidability/undecidability
proof depends very strongly on the formalism being used. One of the reasons for this is that, unlike for simple synthesis, we cannot reduce distributed synthesis problems to the problem of solving a two player game for a simple reason that in the distributed case there are more than two parties.
In this talk we will summarize the existing approaches to synthesis and distributed synthesis problems. We will propose a notion of distributed game that can serve as a common framework for distributed synthesis problems. In such a game there is one environment player and
there is a coalition of process players, each having only a partial information about the play. We will state a couple of results on solvability of such games and indicate why they imply most of the known results for distributed synthesis problems.