Abstracts
Symbolic Analysis of Dynamic Networks of Pushdown Systems
(Joint work with Markus Mueller-Olm (Univ. of Dortmund) and Tayssir Touili (LIAFA, CNRS))
We introduce abstract models for multithreaded programs based on dynamic networks of pushdown systems. We address the problem of symbolic reachability analysis for these models. More precisely, we consider the problem of computing effective representations of their reachability sets using (finite-state) automata-based techniques. We show that, while forward reachability sets are not regular in general (but context-free), backward reachability sets starting from regular sets of configurations are always regular. We provide algorithms for computing backward reachability sets using word/tree automata, and show how these algorithms can be applied for flow analysis of multithreaded programs.
Hybridization methods for verification of non-linear systems
(Joint work with Eugene Asarin (LIAFA, Paris) and Antoine Girard (University of Pennsylvania, Philadelphia)
Recently
hybrid systems, that is systems with both continuous and discrete dynamics,
have proven to be a useful mathematical model for various engineering
applications. Due to the safety critical features of many such applications
(such as avionics, chemical process control), formal verification of
hybrid systems is a topic of particular interest. A common method to
prove a safety property is to compute or over-approximate (if exact
computation is not possible) the reachable set of the system and show
that it does not contain any unsafe states. A major problem in designing
a reachability analysis algorithm for hybrid systems is an efficient
method to handle their continuous dynamics described by differential
equations (since their discrete dynamics can be handled using well-developed
verification methods in computer science). While many well-known properties
of linear differential equations can be exploited to design relatively
efficient methods, non-linear systems are much more difficult to verify.
In this paper, we employ the hybridization approach to the verification
of non-linear continuous systems. The essence behind this approach is
to partition the state space of a complex system into disjoint regions
andthen approximate its vector field in each region by a simpler vector
field. Then, the resulting system is used to yield approximate analysis
results for the original system. For safety verification purposes, the
usefulness of this approach (in terms of accuracy and computational
tractability) depends on the choice of the approximate system. We consider
two classes of approximate systems: piecewise affine and piecewise multi-affine.
We show that the use of these classes allows to approximate the reachable
set of the original non-linear system with a good convergence rate.
Concurrent Secrets
(Joint work with
Eric Badouel, Marek Bednarczyk,Andrzej Borzyszkowski and Benoit Caillaud)
Given a finite state system with partial observers and for each observer,
a regular set of trajectories which we call a secret, we consider the
question whether the observers can ever find out that the trajectory
of thesystem belongs to some secret. We search for a regular control
on the system, enforcing the specified secrets on the observers, even
though they have full knowledge of this control. We show that an optimal
control always exists although it is generally not regular. We state
sufficient conditions for computing a finite and optimal control of
the system enforcing the concurrent secret as desired. We finally point
to applications.
A study of type isomorphisms with application to algorithmics
(Joint work with Tom Leinster)
We
consider the automorphism group of the finitistic (that is, non recursive)
programs on the datatype B = B * B. Specifically, we show that when
* is interpreted as the product type constructor the resulting group
is isomorphic to the group introduced by Richard Thompson known as V.
Further, we also establish that when * is interpreted as a tensor-product
type constructor the resulting group is isomorphic to Richard Thompson's
subgroup of V known as F. As an application, and following Sean Cleary,
we then explain how a well-known finite presentation of the group F
can be used to give an algorithm for transforming any two binary trees
with the same number of leaves into each other by performing rotations
either at the root or at the root's left child.
Tool Support for the Argentum Project
In this talk I presented an overview of the Argentum project, and of the Calculus for Omega Closure Fork Algebras that serves as the homogeneous formalism to which different logics can be translated. I mentioned that the close ressemblance between Omega Closure Fork Algebras and Alloy suggests the use of the latter to analyze properties of the former. Then, I moved to prove that the Calculus for Omega Closure Fork Algebras provides a complete calculus for Alloy too. Finally, I presented the DynAlloy tool and showed that it is better suited than plain Alloy for the analysis of properties of executions of Alloy operations.
References
Frias
M.F., Galeotti J.P., Lopez Pombo C.G. and Aguirre N.,
DynAlloy: Upgrading Alloy with Actions,
in Proceedings of ICSE 2005, St. Louis, USA, May 2005.
Frias
M.F., Lopez Pombo C.G., Baum G.A., Aguirre N. and Maibaum T.S.E.,
Reasoning About Static and Dynamic Properties in Alloy: A Purely Relational
Approach,
to appear in ACM-Transactions on Software Engineering and Methodology
(TOSEM), In press.
Bisimulations up-to for the linear time-branching time spectrum and beyond
(Joint work with Carlos Gregorio Rodriguez)
We present a nice characterization of all the semantics in the linear time branching time spectrum by means of bisimulations up-to that allow acoalgebraic treatment of any of them. The idea is to use the preorder relation generating any of these semantics, instead of the strong bisimulation equivalence that is used in the classical up-to approach. Although this coalgebraic approach is mainly interesting in the case of infinite processes, first we prove our results for finite processess, and then we extend them by applying a continuity result. The ready simulation equivalence, that is rather close to the bisimulation equivalence, represents the limit for our first main theorem. But we also prove a second theorem that gives us the desired characterization for any simulation semantics fulfilling some adequate properties, that we think that distinguish those "good" simulation semantics, having as a consequence many interesting properties. These include for instance the nested simulation semantics, that are stronger than the ready simulation, and therefore were not covered by our first theorem.
Therefore we have in practice a bootstraping mechanism that allows to infer any of the semantic equivalences starting from a part of the corresponding preorders. However the usual way to provide such a initial part of the preorders will be a partial application of the axiomatizations for them. Unfortunately k-nested semantics have no such finite axiomatization, and then it seems not easy to directly apply in practice its coalgebraic characterization. Then we looked for a more modular approach that takes into account the nested character of these semantics. Thus we developed our counting bisimulations, that allow to put together all the nested simulation semantics, characterizing all together by a single bisimulation-like game.
Once again our approach is rather general since it is based in which we call constrained simulations, that generate a family of different semantics, depending on the relation we use as concrete constraint. Whenever such an initial relation is finitely axiomatizable, then all the generalized nested simulation semantics have a common (mutually recursive) conditional axiomatization, which in fact can be seen as a finite (unconditional) axiomatization if the nesting levels are considered as a third argument of a single relation.
Therefore
we have established a common framework to study all the different semantics
in Van Glabbeek's spectrum, including the nested semantics, for which
we have not a finite axiomatization.
Efficient Modeling of Excitable Cells Using Hybrid Automata
We
present an approach based on hybrid automata (HA), which combine discrete
transition graphs with continuous dynamical systems, to modelling complex
biological systems. Our goal is to efficiently capture the behaviour
of excitable cells previously modeled by systems of nonlinear differential
equations. In particular, we derive HA models from the Hodgkin-Huxley
model of the giant squid axon, the Luo-Rudy dynamic model of a guinea
pig ventricular cell, and a model of a neonatal rat ventricular myocyte.
Our much simpler HA models are able to successfully capture the action-potential
morphology of the different cells, as well as reproduce typical excitable
cell characteristics, such as refractoriness (period of non-responsiveness
to external stimulation) and restitution (adaptation to pacing rates).
To model electrical wave propagation in a cell network, the single-cell
HA models are linked to a classical 2D spatial model. The resulting
simulation framework exhibits significantly improved computational efficiency
in modeling complex wave patterns, such as the spiral waves underlying
pathological conditions in the heart.
Satisfiability Checking of Two-way Modal m-calculus and Its Applications
Branching-time
temporal logic can naturally be used to express properties of trees
and graphs, where two-way logic is more useful because it can handle
both forward and backward edges. We have implemented a tableaux-based
satisfiability checker for alternation-free two-way modal mu-calculus
using BDDs (binary decision diagrams) and applied it to schema checking
in XML and shape analysis. In particular, shape analysis can be considered
as tableaux construction with suitable extensions to temporal logic:
two-way, nominal, and global modality.
Deriving Bisimulation Congruences for Graph Transformation Systems
This talk is concerned with the derivation of labelled transitions and bisimulation congruences from unlabelled reaction rules. After a short introduction to categorical constructions such as pushouts and pullbacks, we show how to address this problem in the DPO (double-pushout) approach to graph rewriting. This is done by deriving so-called borrowed contexts as labels. It can be shown that bisimilarity for this labelled transition system is indeed a congruence.
Then,
in the second part of the talk, we compare our work to closely related
work by Leifer/Milner and Sassone/Sobocinski in which labels are derived
using the categorical notion of relative pushout. We explain how problems
with automorphisms can arise in this setting and how they are solved
by the various approaches.
Merged
Processes - a New Condensed Representation of Petri Net Behaviour
(Joint work with
V.Khomenko, A.Kondratyev and W.Vogler)
Model
checking based on Petri net unfoldings is an approach widely applied
to cope with the state space explosion problem. In this paper we propose
a new condensed representation of a Petri net's behaviour called merged
processes, which copes well not only with concurrency, but also with
the other sources of state space explosion, viz. sequences of choices
and non-safeness. Moreover, this representation is sufficiently similar
to the traditional unfoldings, so that a large body of results developed
for the latter can be re-used. Experimental results indicate that the
proposed representation of a Petri net's behaviour alleviates the state
space explosion problem to a significant degree and is
suitable for model checking.
Optimal Controller Synthesis for Real-Time Systems
(Joint work with Patricia Bouyer, Franck Cassez, Alexandre David, Emmanuel Fleury and Didier Lime)
This talk reports on work on controller synthesis for real-time systems through the computation of winning strategies for timed games. Though such games for long have been know to be decidable there has been a lack of efficient, TRUELY on-the-fly algorithms for analyising timed games.
Our work provides an efficient symbolic, forward and on-the-fly algorithm for solving timed games with respect to reachability and safety properties. The algorithm is theoretically optimal having worst-case complexity linear in the underlying region-graph. In practice the algorithm may terminate long before having explored the entire state-space, as its on-the-fly nature allows the algorithm to terminate as soon as a winning strategy has been identified. Also, the individual steps of the algorithm are carried out efficiently by using so-called zones as the underlying datastructure.
A small extension of the algorithm permits time-optimal winning strategies (for reachability games) to be obtained, and the very nature of the algorithm points directly to a distributed version of the algorithm (similar to the distributed version of UPPAAL for reachability analysis of timed automata).
The talk also report an efficient implementation of the algorithm using the DBM-library of UPPAAL experimentally evaluated on a version of the Production Cell.
We
also report on recent results on cost-optimal winning strategies for
games based on priced timed automata. This problem is in general undecidable
-- however under certain non-zenoness assumptions the problem becomes
decidable. Experiments with a prototype implementation in HyTech has
been made.
Integrating
Methods and their Theories for Component Software Modelling, Construction
and Verification
This presentation is about an ongoing research programme on object-oriented
and component-based software development at UNU-IIST. We discuss some
of the concepts, difficulties and significant issues that we need
to consider when developing a formal method for component-based software
engineering. We argue that to deal with the challenges, there is a
need in research to link existing theories and methods of programming
for effective support to component-based software engineering. We
then show initial results about how this can be achieved in the development
in a Relational Calculus, called rCOS, for object and component systems.
Analysis of Modular Arithmetic
(Joint work with Helmut Seidl (Technische Universitaet Muenchen))
More on Verification of Cooperating Traffic Agents
(This
talk presents a continuation of the joint work W. Damm and H. Hungar
reported at the meeting of WG 2.2 in Bertinoro, 2004.)
We decompose the proof of collision freedom of cooperating traffic agents
like trains, cars and airplanes by devising a general proof rule that
can be instantiated with concrete applications. In our approach an agent
is modelled as a parallel composition of a plant and a controller each
one represented as a hybrid automaton.
The proof rule exploits a coordination protocol that is typical for achieving collision avoidance and makes use of concepts like safety envelopes and criticality measures. The proof rule has a number of premises each of which, we argue, is substantially easier to verify than the global property of collision freedom. We formalise the proof rule for the case of two traffic agents in the State Transition Calculus, an extension of the Duration Calculus that can represent both interval based state properties and instantaneous transitions, and prove its soundness.
As an application we consider a train gate scenario and show how it can be viewed as an instantiation of the general proof rule, thus proving collision freedom.
Game
Semantics and Software Model Checking
Game semantics is a way of giving meanings to programming languages using simple and intuitive notions of game playing. The approach goes back to Kleene and Gandy in one tradition, and to Kahn and Plotkin, and Berry and Curien in another. Compared to other semantics of programming languages, a striking feature of game semantics is that it is denotational (and so admits compositional methods) and yet has clear operational content; further it gives rise to highly accurat (fully abstract) models for a wide range of programming languages.
A recent
development in game semantics is concerned with the algorithmic representation
of fully abstract game semantics, with a view to applications in software
model checking and program analysis. The goal is to build on the tools
and methods which have been developed in the Verification community,
while exploring the advantages offered by our semantics-based approach.
In this talk, we present a complete classification of the decidable
(with respect to observational equivalence) fragments of a higher-order
procedural language, and briefly survey applications of the approach
to program verification.
Probabilistic and Nondeterministic Aspects of Anonymity
(Joint
work with Mohit Bhargava)
The concept of anonymity comes into play in a wide range of situations,
varying from voting and anonymous donations to postings on bulletin
boards and sending mails. The systems for ensuring anonymity often use
random mechanisms which can be described probabilistically, while the
agents' interest in performing the anonymous action may be totally unpredictable,
irregular, and hence expressable only nondeterministically.
Formal definitions of the concept of anonymity have been investigated in the past either in a totally nondeterministic framework, or in a purely probabilistic one. In this paper, we investigate a notion of anonymity which combines both probability and nondeterminism, and which is suitable for describing the most general situation in which both the systems and the user can have both probabilistic and nondeterministic behavior. We also investigate the properties of the definition for the particular cases of purely nondeterministic users and purely probabilistic users.
We formulate our notions of anonymity in terms of observables for processes in the probabilistic $\pi$-calculus, whose semantics is based on Probabilistic Automata.
We
illustrate our ideas by using the example of the dining cryptographers.
Deductive and Inductive Methods for Program Synthesis
(Joint
work with Elena Sanko, Insitute of Cybernetics, Tallinn, Estonia)
Formal specifications that define required system properties play a
central role in software engineering. They can be used for reasoning
about complex programs on a suitable abstract level. Formal models are
inescapable when programs are automatically derived or verified. The
most widely used techniques for automatic program construction are based
on stepwise refinement of a specification until a program code is achieved.
In this talk, the different approaches are considered for program generation where programs are obtained by means of special mathematically based manipulations, without construction of intermediate level specifications. In particular, we briefly introduce a method based on proof search, known as structural synthesis of programs (SSP), and on the other hand, a technique based on the optimization of a specific fitness function related to the task to be solved. SSP has been implemented in a couple of commercial and some experimental systems that are basically of scientific or pedagogical value. SSP's most advanced implementation is in the system NUT performed jointly by the researchers of the Institute of Cybernetics (Tallinn) and Deparment of Teleinformatics of KTH.
The
SSP method is a deductive approach for program synthesis carried out
via special logical inference rules from a general relational specification
of a problem. This specification is often called the computational model
of the problem. Here we are going to design an inductive approach for
automatic program construction based on the same specification language
(computational model) that is augmented by experimental data that describe
desirable input-output behavior of the program to be composed. A common
specification would bridge deductive and inductive methods of program
construction. We believe that combining these two types of techniques
might provide more general and effective procedures for automation of
software development. This would simulate human reasoning where deductive
inference steps are interleaved with drawing conclusions from samples
of experimental data. In the talk we will introduce the idea of inductive
program construction as well as an algorithm for coding sequential programs
by real numbers that allow transforming a task for program synthesis
into an optimisation problem that could be solved using evolutionary
programming techniques.
A Calculus of Mobile Broadcasting Systems
Computers often send messages broadcast over ethernets, and point-to-point between them: globally asynchronous, locally synchronous. This paradigm inspires the new primitive calculus presented here, MBS (mobile broadcasting systems). MBS processes communicate by broadcast, but only in {\em rooms}, and move between rooms at unspecified speeds. A broadcaster is heard instantly by everyone else in the room, but by no one outside. Priorities are attached to speech and to exits from rooms, and rooms can be blocked awaiting a message; these primitives suffice to synchronise broadcasting and moving. MBS borrows the treatment of names from the $\pi$-calculus, but the latter's ``get/put $b$ on channel $a$'' becomes in MBS ``go to $a$ and hear/say $b$''.
Truth by Evidence
We
introduce a new theory of expressions where expressions are divided
into the two categories of objects and judgments. The universe of expressions
is open ended and we can develop mathematics step by step by adding
new constants for objects and jugments. We assign meaning to judgments
by defining what is an {\em evidence} for a given judgment. We also
give a short demonstration of the computer environment CAL/NF for formally
developing mathematics which is based on our theory of expressions.
Observability, Connectivity, and Replay in a Sequential Calculus of Classes
Object calculi have been investigated as semantical foundation for object-oriented languages. Often, they are object-based, whereas the mainstream of object-oriented languages is class-based.
We
formulate an operational semantics that incorporates the connectivity
information into the scoping mechanism of the calculus. Furthermore,
we formalize a notion of equivalence on traces which captures the uncertainty
of observation caused by the fact that the observer may fall into separate
groups of objects. We use a corresponding trace semantics for a simple
notion of observability. This requires to capture the notion of \emph{determinism}
for traces where classes may be instantiated into more than one instance
during a run and showing thus twice an equivalent behavior (doing a
``replay''), a problem absent in an object-based setting.
Keywords:class-based object-oriented languages, formal semantics, determinism,
full abstraction
Checking Atomicity in Concurrent Java Programs
Atomicity is a common correctness requirement for concurrent programs. It requires that concurrent invocations of a set of methods be equivalent to performing the invocations serially in some order. This is like serializability in transaction processing. Analysis of atomicity in concurrent programs is challenging, because synchronization commands may be scattered differently throughout each program, instead of being handled by a fixed strategy, such as 2-phase locking.
We
are developing techniques for checking atomicity in concurrent programs,
using static analysis, dynamic analysis (run-time monitoring), and novel
combinations of them. This talk surveys our research in this area, discusses
trade-offs between different techniques, and describes our experience
applying them to about 40 KLOC of Java programs.
On
the synthesis of correct by design embedded control software.
Current state of the art technology has fostered the pervasive use of
microprocessors in our every day life. Examples include portable accessories
such as mobile phones and PDA's; home appliances such as refrigerators,
toasters and coffee machines; medical equipment such as defibrillators,
dialysis machines and MRI?s among many other systems. These embedded
computing devices interact with the continuous environment in nontrivial
ways that difficult its analysis and synthesis. In this talk I will
focus on the problem of synthesizing embedded controllers that are provably
correct by design. This approach contrasts with current techniques where
verification plays an important role in ensuring correctness of operation.
I will show how it is possible to automatically design controllers from
discrete specifications (languages, finite state machines, temporal
logics, etc) for purely continuous systems and how these results lead
to embedded control software. One novelty of this approach is the fact
that we synthesize both continuous control laws and a description of
its software implementation resulting in embedded control systems that
are correct by construction.
Compositional natural semantics, Hoare logics and type systems for low-level languages
(Joint work with Ando Saabas, Institute of Cybernetics, Tallinn)
Low-level languages, where a piece of code is a flat set of labelled instructions with no explicit phrase structure, have traditionally been considered inherently non-modular and therefore hard to reason about. But the advent of the paradigm of proof-carrying code (or, more generally, certified code) has generated significant renewed interest in reasoning about low-level code. We show that the seemingly banal implicit and ambiguous structure of finite unions of pieces of code with non-overlapping support makes a phrase structure which, if properly exploited, is perfectly reasonable both from the viewpoint of metatheory and with the view on practical reasoning about large pieces of software. We show how this phrase structure leads to compositional natural semantics, Hoare logics and type systems with beautiful metatheoretical properties. Among other things, the approach supports compilation of proofs together with programs. This is new work, which has been partially reported upon at SOS 2005, but is ongoing. Some new work by Tan and Appel as well as Benton is related, but our approach is, we claim, substantially simpler and neater.
Alternating Timed Automata
(Joint work with Slawomir Lasota)
A notion
of alternating timed automata is proposed. It is shown that such automata
with only one clock have decidable emptiness problem. This gives a new
class of timed languages which is closed under boolean operations and
which has an effective presentation. It is shown that the complexity
of the emptiness problem for alternating timed automata with one clock
is non-primitive recursive. The proof gives also the same lower bound
for the universality problem for nondeterministic timed automata with
one clock thereby answering a question asked in a recent paper by Ouaknine
and Worrell. Undecidability of the emptiness problem over infinite words
is also shown.
Investigation of Discrete Event Systems by Means of Dynamical Systems. Application to Concurrency.
There
has been a huge amount of interesting work done in the field of hybrid
systems. A lot of attention has been paid to extending the existing
techniques developed for analysis of discrete event systems to tackle
the dynamics; one of many examples is a hybrid automata. As a person
devoted to the dynamical systems and their application in control engineering
I will attack the problem from the opposite point of view. I tackle
discrete event systems with tools developed for the geometric theory
of dynamical systems. The case study I will consider in this talk is
the concurrency and the objective is to classify executions of a concurrent
program. I will treat a computer program as a flow line of a vector
field. The flow line is born at a point p, which is the start of the
program, and dies at a point q, the end of the program. Due to different
scheduling scenarios the execution of the same program may result in
flow lines of vector fields close to each other.
