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 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 Related
Paper :
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 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 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 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
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
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 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 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.
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 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 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 In
an earlier report : 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 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 Distributed
games |
|