abstract

We present different techniques for exact/approximate computation of the reachability sets in this framework. Some of the techniques are precise for significant classes of models, and others are generic techniques for abstract analysis in the general case. We illustrate this approach by showing its application in program verification, in particular in the case of sequential programs manipulating dynamic linked lists, and in the case of multithreaded programs with recursive procedures.

Rocco De Nicola

On the Expressive Power of Klaim-based Calculi

(Note: joint work with Daniele Gorla and Rosario Pugliese)

In the talk we presented the investigation of the expressive power of variants of Klaim, an experimental language with programming primitives for global computing that combines the process algebra approach with the coordination-oriented one. Klaim has proved to be suitable for programming a wide range of distributed applications with agents and code mobility, and has been implemented on the top of a runtime system based on Java. We have tested the expressivity of its constructs by distilling from it some, simpler and simpler calculi and by studying the encoding of each of the considered languages into a simpler one. An encoding of the asynchronous pi-calculus into one of the presented calculi. We also presented a series of properties enjoyed by the different encodings.

Mariangiola Dezani-Ciancaglini

Boxed Ambients with Communication Interfaces

(Note: joint work with Eduardo Bonelli, Adriana Compagnoni, and Pablo Garralda)

We define BACI (Boxed Ambients with Communication Interfaces), an ambient calculus allowing a liberal communication policy. Each ambient carries its local view of the topic of conversation (the type of the information being exchanged) with parents and children that will condition where it is allowed to stay or migrate to and which ambients may be allowed to enter it. The topic of conversation view of ambients can dynamically change during migration. BACI is flexible enough to allow different topics of conversation between an ambient and different parents, without compromising type-safety: it uses port names for communication and ambient names for mobility. Capabilities and co-capabilities exchange port names and run-time typing information to control mobility. We show the type-soundness of BACI proving that it satisfies the subject reduction property. Moreover we study its behavioural semantics by means of a labelled transition system.

Cédric Fournet

Verifying Web Services Security

(Note: Joint work with Karthik Bhargavan and Andy Gordon)

We consider the problem of verifying cryptographic security protocols for XML web services. The security standard WS-Security specifies a range of XML security tokens, such as username tokens, public-key certificates, and digital signatures, amounting to a flexible vocabulary for expressing protocols.

To describe the syntax of these tokens, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates to describe the semantics of security tokens and of sample protocols distributed with the Microsoft WSE implementation of WS-Security. By embedding our data model within the applied pi calculus, we formulate security properties with respect to a standard Dolev-Yao threat model. We then automatically check these properties using protocol verifiers. To the best of our knowledge, this is the first approach to the verification of security protocols based on a faithful account of the XML wire format.

Relying on WS-Security, the WS-SecurityPolicy specification provides a declarative configuration language for selecting security mechanisms
in web services implementations. Accordingly, we develop a formal semantics for WS-SecurityPolicy in our model, and propose a more abstract link language for specifying simple security goals of web services and their clients. We finally present a series of automatic tools that can

Papers and additional information are available from http://Securing.WS

Marcelo Frias

The Argentum Project

Argentum is a CASE tool with relational foundations under development by the group of Relational Methods at the Department of Computer Science of the University of Buenos Aires. Rather than using a single monolithic language for software specification, it uses different logics for modelling different views of systems. Thus a system specification becomes a collection of theories coming from different logics. Using the interpretability results for these logics, the theories are translated to a uniform relational specification. Once this is obtained, different tools such as model checkers or theorem provers can be applied in order to verify the relational specification.

David de Frutos Escrig
Ready Simulation Equivalence as a Global Bisimulation

(note : joint work with Carlos Grigorio Rodriguez)

Maurizio Gabbrielli

Comparing Recursion and Replication in Process Calculi

(Note: joint work with Nadia Busi and Gianluigi Zavattaro)

We investigate the expressive power of two alternative approaches used to express infinite behaviours in process calculi, namely, replication and recursive definitions. These two approaches are equivalent in the full pi-calculus, while there is a common agreement that this is not the case when name mobility is not allowed (as in the case of CCS), even if no formal discriminating results have been proved so far.

We show that one can deterministically encode a Random Access Machine (RAM) in CCS with recursion, hence both the existence of a terminating computation and the existence of a diverging computation are undecidable properties in this calculus. On the other hand, we show that only a non deterministic encoding of RAM is possible for CCS with replication, since the existence of a diverging computation is a decidable property in this case.

We also consider other two properties, namely weak bisimulation and the ability to perform a synchronization on a certain channel after a (possibly empty) internal computation (barb). We prove that weak bisimulation is undecidable in both the calculi, while barb is undecidable in CCS with recursion and is decidable in CCS with replication.

Finally we show that recursion, replication and iteration (a third possible way to add infinite behaviours) constitute a strict expressiveness hierarchy w.r.t. weak bisimulation: namely, there exist weak bisimulation preserving encodings of replication in recursion (and of iteration in replication), whereas there exist no weak bisimulation preserving encoding in the other direction.

Radu Grosu

Monte Carlo Model Checking

(Note: joint work with S.A. Smolka)

We present $MC2$, what we believe to be the first randomized, Monte Carlo algorithm for temporal-logic model checking, the classical problem of deciding whether or not a property specified in temporal logic holds of a system specification. Given a specification $S$ of a finite-state system, an LTL (Linear Temporal Logic) formula $\varphi$, and parameters $\epsilon$ and $\delta$, $MC2$ takes $N=\ln(\delta)/\ln(1-\epsilon)$ random samples (random walks ending in a cycle, i.e\/ \emph{lassos}) from the B{\"u}chi automaton $B=B_S \times B_{\neg\varphi}$ to decide if $L(B)=\emptyset$. Should a sample reveal an accepting lasso $l$, $MC2$ returns false with $l$ as a witness. Otherwise, it returns true and reports that with probability less than $\delta$, $p_Z\geq\epsilon$, where $p_Z$ is the expectation of an accepting lasso in $B$. It does so in time $O(N \cdot D)$ and space $O(D)$, where $D$ is $B$'s recurrence diameter, using a number of samples $N$ that is optimal to within a constant factor. Our experimental results demonstrate that \mc is fast, memory-efficient, and scales very well.

Alexander Knapp

Model Checking UML State Machines and Collaborations

The "Unified Modeling Language'' (UML) provides two complementary notations, state machines and collaborations, for the specification of dynamic system behavior. We describe a prototype tool, Hugo/RT, that is designed to automatically verify whether the interactions expressed by a collaboration can indeed be realised by a set of state machines. Hugo/RT can handle untimed behaviour by a translation into the on-the-fly model checker Spin, and also timed behaviour by a translation into the real-time model checker Uppaal. We discuss two alternative translation schemes for UML state machines: an approach based on the intermediate language SMILE which retains the hierarchical features of state machines; and a flattening approach which discards the hierarchy of state machines but in general leads to a faster model checking procedure. A UML interaction in an collaboration is translated into either a Spin "never claim'' or an observer timed automaton.

Barbara Koenig

A General Framework for Types in Graph Rewriting

A general framework is presented which can be instantiated in order to obtain type systems for graph rewriting, allowing us to statically infer behavioural properties of a graph. We describe conditions such as the subject reduction property and compositionality that should be satisfied by such a framework. A methodology for proving these conditions is presented, specifically it is shown that it is sufficient to prove properties that are local to graph transformation rules. In order to demonstrate the applicability of this framework, case studies show how to integrate existing type systems for the pi-calculus and the lambda-calculus.

Maciej Koutny

Applying Petri Net Unfoldings in System Design

The behaviour of asynchronous circuits is often described by Signal Transition Graphs (STGs), which are Petri nets whose transitions are interpreted as rising and falling edges of signals. One of the crucial problems in the synthesis of such circuits is that of identifying whether an STG satisfies the Complete State Coding (CSC) requirement, e.g., by using model checking based on the reachability graph of an STG.

In the approach presented in this talk, we avoid constructing the reachability graph of an STG, which can lead to state space explosion, and instead use only the information about causality and structural conflicts between the events involved in a finite and complete prefix of its unfolding. The model checking algorithm is derived by adopting the Boolean Satisfiability (SAT) approach. In the second part of the talk, we outline how an extension of this approach can be used to synthesise asynchronous designs.

The proposed technique leads not only to huge memory savings when compared to methods based on reachability graphs, but also to significant speedups.

Stephan Merz

Refinement of events with permissions and obligations

In the context of security-sensitive systems, it becomes important to describe the conditions under which events are allowed to happen or,
dually, become obligatory. For example, in a hospital application, a nurse will have different access rights than the treating physician, and the precise conditions may depend on factors such as the time of day. Whereas several frameworks exist to represent permissions and obligations, based on the views of roles, activities, and organizations, few formal development methods reflect such "deontic" notions in their notions of correctness and refinement.

In this talk, we propose an extension of event systems (as in action systems [1] or B event systems [2]) by fairness conditions and
permissions. User rights, interdictions, and obligations are represented by linear-time properties, and can be verified using standard proof rules. Standard notions of refinement are shown to preserve interdictions and obligations, even when modifying the grain of atomicity. We also propose a verification condition that combines permissions and obligations at the lower level to preserve permissions at the higher level.

[1] R. Back, J. von Wright: Refinement calculus -- a systematic introduction. Springer-Verlag, 1998.

[2] J.-R. Abrial: Event Driven System Construction. Internal report (1999).

Ugo Montanari

Multi-Party Synchronization with Mobility for Graph Transformations

(Note: joint work with Ivan Lanese)

In the talk we introduce a generalization of synchronization algebras, able to deal with mobility and local resource handling. We apply this generalized notion to Synchronized Hyperedge Replacement, a graph transformation formalism whose transitions are obtained by synchronizing local context-free productions. The result is a powerful model that allows concurrent multi-party synchronizations with mobility, where synchronizations are performed according to the specification provided by the synchronization algebra. We present the operational semantics for the model, and an abstract semantics based on bisimilarity. We also prove that this abstract semantics is a congruence w.r.t. the operators of an axiomatization for graphs in the style of Bauderon and Courcelle. Finally, we use our formalism to model the Fusion Calculus, thus defining a concurrent semantics for it.

Ernst-Ruediger Olderog

Towards Verification of Cooperating Traffic Agents

(Note: joint work with W. Damm and H. Hungar)

We exploit design patterns employed in coordinating autonomous transport vehicles to reduce the burden in verifying cooperating hybrid systems. The presented verification methodology is equally suited for train applications (such as ETCS), avionics applications (such as TCAS), or automotive applications (such as platooning).

We present a first version of a verification rule explicating the essence of employed design patters and guaranteeing the global safety property of collision freedom, whose premises can either be established by off-line analysis of the worst-case behavior of the involved traffic agents, or by purely local proofs, involving only a single traffic agent. In the talk the verification method (but not yet the verification rule) is applied to a train gate scenario. The scenario is formalised in the State Transition Calculus, a variant of the Duration Calculus.

Reference :
W. Damm, H. Hungar and E.-R. Olderog.On the Verification of Cooperating Traffic Agents. To appear in: Proc. FMCO'03, LNCS-Series, Springer-Verlag, 2004.

Wojciech Penczek

Model Checking Multi-Valued Modal mu-Calculus: Revisited

(Note: joint work with B. Konikowska)

We show that the general method of translation between De Morgan algebras can be extended to mv modal mi-calculus model checking. We prove that the translations by Gurfinkel and Chechik as well as by Godefroid and Bruns can be viewed as its special case when the target algebra is two-valued. We improve on this translation by identifying a new condition for the duplication of the states of a model to be unnecessary. This is the case when the general translation preserves not only upper and lower bounds, but also complement. We give several examples supporting practical applicability of our improvement, but show also that for several algebras there are translations to the two-valued case that do not preserve complement. Motivated by that fact and by the existence of efficient model checkers over 3-valued algebras, we investigate translations to such an algebra. We show that for many of the commonly used algebras one can define a translation which preserves complement in addition to all the bounds. This result suggests that in practice one should consider translations to 3-valued algebras as well.

Anders P. Ravn

Quantitative Aspects of Components

(Note: joint work with Jens P. Holmegaard and Peter Koch)

Much research on component based systems is aimed at giving function or behavioural specifications for components in such a form that the result of assembling individual components has properties that are derivable from the ones specified for the individual constituents of the assembly. For embedded systems, functionality and behaviour is not enough to specify a satisfactory solution. Quantitative aspects are also part of the requirements. A prime example of such a quantitative aspect is timing, either in the form of hard real-time constraints or constraints on the quality of service. For a discussion of these issues we refer to part II in [1]. In some applications, classical resources like memory (data and program) and even power consumption is also a primary constraint. Currently the main technique for assessing such constraints is simulation of an implementation which is both time consuming and costly in development. In [2] we investigate a framework for estimating such properties by abstract interpretation of the structure of the assembly. The investigation includes a prototype tool for analyzing such properties of a SystemC program.

[1] Selected topics in Embedded SystSeleems Design: Roadmaps for Research, ARTIST IST-2001-34820.

[2] An Approach to Quality Estimation in Model-Based Development, In Proceedings of Workshop on Model-Based Methodologies for Pervasive and Embedded Software (MOMPES 2004), T UCS General Publication 29, Turku Centre for Computer Science, pp.81-92, May 2004.

Wolfgang Reisig

The Contribution of Abstract State Machines to the Foundations of Formal Specification

After many years of research and exercise towards adequate modeling languages, the question arises as to whether there exists a theoretical
foundation of "specification", in analogy to the computable functions, which provide the foundation of programming. Conventional semantics is based on states s: var ? val, where var and val are sets of variables and values, respectively. A run is a finite or infinite sequence of states, and a specification is a finite description of a set of runs. Conventional semantics is based on the assumption that each value is a finite or infinite sequence of symbols. The specification is implementable in this case. We are interested in the case where values are any items. Examples are the basic objects of midleware programs. Toy examples are geometrical algorithms with points, circles, lines etc as basic elements, and
operations such as the construction of a line from two nodes, or the intersection points of intersecting circles. An adequate description of a specification of this kind is based on a signature ?; viz. a collection of operation symbols, each with its arity. A specification is then essentially a ?-term, and a state is a ?-structure. This is in fact the basics of Gurevich's Abstract state machine approach. This proposal may eventually be an adequate starting point for a theory of specification.

Davide Sangiorgi

The origins of bisimulation and coinduction

In the talk i will discuss the origins of the notions of bisimulation and coinduction, in Computer Science and elsewhere, and related concepts such as greatest fixed points, least fixed points, and the main fixed-point theorems.

Roberto Segala

Axiomatizations for Probabilistic Automata

We study the relationship between the alternating and non-alternating models of nondeterministic stochastic systems with the double aim of comparing the models and of accessing their strength. For the purpose we describe a simple process algebra, to which we give an alternating as well as a non-alternating operational semantics, and we study axiomatizations for bisimulation and trace-based equivalences and preorders. We show that the alternating model can be seen as a special case of the non-alternating model and we show that our axiomatizations are simple and consistent with the corresponding axiomatizations for purely nondeterministic systems. This shows that the choices behind the two models are likely to be along the right direction.

Martin Steffen

Observability, Classes, and Object Connectivity

(Note: joint work with Erika Abraham, Marcello Bonsangue and Frank de Boer)

The concurrent object calculus has been investigated as a core calculus for imperative, object-oriented languages with multithreading and heap-allocated objects. The combination of this form of concurrency with objects corresponds to features known from the popular language \Java. One distinctive feature, however, of the concurrent object calculus is that it is \emph{object-based}, whereas the mainstream of object-oriented
languages is \emph{class-based.}

This work explores the semantical consequences of introducing classes to the calculus. Considering classes as part of a component makes
instantiation a possible interaction between component and environment. A striking consequence is that in order to characterize the observable
behavior we must take \emph{connectivity} information into account, i.e., the way objects may have knowledge of each other. In particular, unconnected environment objects can neither determine the absolute order of interaction and furthermore cannot exchange information to compare object identities.

We formulate an operational semantics that incorporates the connectivity information into the scoping mechanism of the calculus. As instantiation itself is unobservable, objects are instantiated only when accessed for the first time ("emphlazy instantiation'').

Furthermore we use a corresponding trace semantics for full abstraction wrt. a may-testing based notion of observability.

Andrzej Tarlecki

Software Specification and Development in Heterogeneous Environments

The overall idea of the talk is to present recent work aimed at dealing with multiple logical systems in a single specification and
software development task. I first recall the basic technical notions related to modelling logical systems as institutions, presenting them using (model-theoretic) parchments, relating institutions and parchments using morphisms of various kinds, etc. Given this background, I discuss in some detail the possibilities for combining logical systems using standard categorical constructions in the category of either institutions or parchments. Some positive results (like completeness of the relevant categories) are given. However, these do not lead to miraculous combinations of any possible logical features, but rather provide a framework which limits the necessary ingenuity (and human decisions) to some specific points, and hint at possible techniques of formulating the necessary decisions in the most effective way. Then, I sketch how the mechanisms of various mappings between institutions may be used to cater for heterogeneous specifications, which span an number of linked institutions, and for the description of the development process which may 'migrate' between various institutions in the course of development of separate modules of the system. Overall, a picture of a heterogeneous logical environment for software specification and development is emerging as as simply a diagram of institutions linked by morphisms of various kinds.