Amsterdam, The Netherlands, 14 - 17 May 2003
Abstracts
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.
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
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.
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.
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)
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
presented.
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.
(Linear)
Algebra for Program Analysis 
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.
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.
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.
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 www.cwi.nl/~janr)
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.
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.
