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.
(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.
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.
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.
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.
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.