General
Committees
Workshop
Useful Links
Invited speakers
- Mario Bravetti, Universita di Bologna, Italy
- Assaf Kfoury, Boston University, USA
- Guy Juanole, LAAS Toulouse, France
- Joel Ouaknine, Oxford University, United Kingdom
Foundational aspects of contract compliance and choreography conformance
A choreography is the description of the behaviour of a group of interacting participants. Two main approaches are considered in the context of service oriented computing for the description of choreographies, the WS-CDL approach (expressing the global view of participant interactions) and the BPEL4Chor approach (describing the sequence of invoke and receive operations executed by each participant). Given a choreography, expressed in one of the two approaches, we consider the problem of independently retrieving services that, once combined, correctly implement the choreography. The theory that we propose to address this problem assumes that each available service publishes its externally observable message passing behaviour in a so-called service contract. In order to check whether a service correctly implements a given participant in a choreography, we first extract from the choreography description the contract representing that participant, then we check whether the contract of the considered service refines it. We perform a theoretical study of the coarsest refinement relation: it turns out to be a variant of must/fair testing.
Lightweight Formal Methods for the Development of High-Assurance Networking Systems by Assaf Kfoury
A description of the talk will be availabe later.
Networked Control Systems by Guy Juanole
In the technological context of today, distributed computing systems (computers interconnected through a communication network) are more and more used , in particular in the industrial world, for implementing distributed physical process control applications ( applications constituted of three remote tasks(sensor, controller, actuator) and based on a closed loop structure i-e with a feedback). Such systems which implement remote Control over Networks are called Networked Control Systems (NCS). The distributed physical process control applications have time constraints (constraints coming from the dynamic of the physical processes to observe and to control) and then require that the underlying distributed computing system be real time i-e provides (for the execution of the implicated different tasks ( sensor, controller, actuator) and for the transfer of the flows between these tasks ( flow sensor-controller, flow controller-actuator)) a timeliness Quality of Service (QoS)in order to guarantee a good Quality of Control (QoC). The QoS depends on the operational mechanisms of the distributed computing system and, in particular, on basic mechanisms of the computers (task scheduling) and of the communication network ( message scheduling, data transfer protocol).The QoC depends on the QoS and on the control law associated to the physical process . The study and the design of the NCSs represent today an area of research very important because of its multidisciplinary characteristic which requires deep knowledge in Automatic control, Communication networks and Computers. The goal of this presentation is to present some works which concern the evaluation of the QoC of a distributed process control application. We want to present two types of works:
- the first type is based on a distributed computing
system which is specified independently of the control
applications ( this kind of work is representative of what was
done still till the last years); the QoS is evaluated ( for
example, using formal description techniques ) and the value of
the Qos is injected in the equations which give the QoC. This
study shows results obtained with different local wired and
wireless networks,
- the second type considers the whole
system as an integrated system ( in particular, by considering a
priority scheme for scheduling the messages , the priority is
now a function of the performances of the control application).
This study, which shows the interest of such a co-design view,
is representative of the works of today
Verifying Probabilistic Programs: Three Easy Pieces by Joel Ouaknine
I will present some recent work on automated verification of probabilistic programs and randomised algorithms, using a simple procedural probabilistic programming language for which we have built an equivalence checker, called APEX. I will illustrate our approach with three non-trivial case studies: (i) Herman's self-stabilisation algorithm; (ii) an analysis of the average shape of binary search trees obtained by sequences of random insertions and deletions, inspired by a paper of Don Knuth; and (iii) the famous problem of anonymity in David Chaum's Dining Cryptographers protocol.
This is joint with Axel Legay, Andrzej Murawski, and James Worrell.