9:00 - 9:05: Welcome
9:05 - 10:30: 1st Session
9:00 - 10:30 : Session
Abstracts
Pierre Corbineau : Equality and equivalence relations in formal proofs
The talk will start with an introduction to my previous research work
and an outline of my oncoming research interests, followed by a
current research subject of mine: the automation of equivalence
reasoning in Higher-order formal proof systems.
Equivalence relations are pervasive in formal proofs where objects
have no natural canonical form, and hence where the Leibniz equality
is too fine-grained. The distinction between equality and a standard
equivalence relation lies in the replacement rule: replacement by
equals is valid anywhere, whereas equivalent objects can only be
replaced in appropriate contexts. I will give a formal definition of
these relations and show how a standard equality proof technique,
namely congruence-closure, can be extended to solve problems with an
arbitrary number of equivalence relations.
Jan Olaf Blech:
Certifying Deadlock-freedom of BIP Models -- a Case Study for the
Certifcation of Safety Critical Software
Certificates can be used to encapsulate and guarantee properties of
software systems. We focus on using them to guarantee the correctness
of properties discovered by potentially large untrusted verification
tools. These tools are hard or impossible to verify themselves. We
motivate that generating certificates, which contain a proof for the
correctness of a concrete analysis result of a verification tool for a
given system is the easier task for guaranteeing correctness of these
results. Checking certificates independently by a small trusted
certificate checker (a higher-order theorem prover), lifts untrusted
analysis results to the high level of trust the higher-order theorem
prover ensures.
In this talk we report on our work on extending the D-Finder tool for
detecting deadlocks in BIP models with a certificate generation and
checking infrastructure using the Coq theorem prover. In addition to
this case study, we present our work towards a general methodology for
the usage of certificates in software analysis and development and
discuss potential benefits.
Matthieu Gallien : Toward a More Dependable Software Architecture for Autonomous Robots
I will present the existing work done in the LAAS laboratory about software
architecture for autonomous robots. There has been more than 15 years of
research in this field. This approach has been mostly focused on getting the
robots to do what they have to. For example, good algorithms for autonomous
navigation has been developed and integrated on several robots. There has been
tools and methodology created for ease of integration of algorithm into the
software architecture of the robot. There has been success, however there is
no way to verify or validate this architecture. We have proposed a combined
approach that builds on the existing architecture and method and uses BIP to
build models of the softwares, validate and generate code to be executed on
the robot. This has been tested and integrated on one robot and tested at
LAAS. We have shown that it is possible to have a formal model of the
software, to validate and verify it and to generate code that works.
NGUYEN Tranh-Hung
D-Finder: A Tool for Compositional Deadlock Detection and Verification
Abstract: D-Finder is a tool that supports the verification of
invariance properties and deadlock detection. It implements a
compositional method for the verification of component-based system
described in BIP language encompassing multi-party interaction. The
method is based on the use of two kinds of invariants. Component
invariants which are over-approximations of components' reachability
sets. Interaction invariants which are constraints on the states of
components involved in interactions. Interaction invariants are
obtained by computing traps of finite-state abstractions of the
verified system. The obtained experimental results for non trivial
case studies show the capabilities of D-Finder as well as the
efficiency of the method.
Ylies Falcone: Enforcement Monitoring wrt. the Safety-Progress Classification of Properties
Abstract :
Current development techniques for information systems are often based
on component software re-use. These components tend to come from
third-party. Whereas this approach is desirable from a software
engineering perspective and productivity, it raises up some security
problems for the global application. A possible approach to solve this
problem consists in monitoring each component behavior against a
global security policy. Besides simple error detection, such monitors
can also ensure a correct component behavior by modifying its
interactions with the rest of the application. This is the so called
enforcement monitoring approach of security policies. This technique
is very encouraging and it has been already implemented in some
applications.
We have extended previous works on this topic in several
directions. Firstly, we have proposed a generic notion of enforcement
monitors based on a memory device and finite sets of control states
and enforcement operations. Moreover, we specified their enforcement
abilities wrt. the general safety-progress classification of
properties. Furthermore, we have proposed a systematic technique to
produce an enforcing monitor from the recognizing automaton. Finally,
we have developed a prototype toolbox implementing the proposed
features.
GARNIER Florent:
Termination of fair execution v.s. Positive Almost sure termination of
infinite state programs under probabilistic fair
schedulers. Application to the verification of randomized distributed
concurrent communication protocols.
In recently submitted work, we use term rewriting as a formalism to model
countable state space program, possibly infinite. We define a notion of fair
execution and we characterize the set of programs that only admit finite
length fair executions. In this context, fairness means that if a program
visits infinitely often a state or a configuration, then it will visit all
this state possible successors. This notion of fairness is highly
non-deterministic, and can't be used to implement a deterministic scheduler
that handles choices or interleaving. We define a model of reasonable
randomized fair strategy, that handles such choices, and we show that a
program modeled by a term rewrite system has all its fair execution of
finite length, if and only if under all reasonable fair randomized strategy,
this program terminates with probability one, within a finite mean number of
computation steps. We explain why such an equivalence is relevant in the
sense it allows to implement finite memory --even memoryless-- schedulers
that will lead a program to termination.
DAUBIGNARD Marion: Towards a proof system for computational indistinguishability
Provable security is now an important line of research in
cryptography. Various security criteria have been defined to suit many
kinds of cryptosystems and capture such or such aspect of their
security. Most of these criteria rely on the underlying concept of
indistinguishability. This accounts for our focusing on designing
inference rules to prove indistinguishability of distributions. We
will start by defining the framework in which the proofs are to be
carried out, and will then give the main ideas about the design of our
system of rules. (This is a joint work with Yassine Lakhnech and
Bruce Kapron).
Lilia Sfaxi: Construction de composants surs : Le modèle
CIF (Component Information Flow)
Les modèles de composants sont de plus en plus utilisés
dans la construction des systèmes répartis grâce à leur
modularité qui facilite le développement et
l'administration de ces systèmes. Néanmoins, les
concepteurs de systèmes à base de composants se contentent en
général de fournir des propriétés de
sécurité classiques comme l'authentification et le
cryptage de la communication entre composants ; d'autres aspects
avancés de la sécurité sont ignorés telle
que la propriété de non interférence.
CIF (Component Information Flow) a pour objectif de garantir la
propriété de non interférence à une plus grande
granularité, celle des composants. Ceci est
réalisé en fournissant les outils de configuration des
paramètres de sécurité des composants, un
compilateur vérifiant la propriété de non
interférence ou complétant, quand c'est possible, cette
configuration si elle est inachevée. Quand la configuration est
validée, CIF génère automatiquement les
composants et les liaisons assurant les propriétés de
sécurité définies à la configuration.
Matthieu Gallien: Data Flow Embedded Systems: DOL to BIP Translation
DOL (Distributed Operation Layer) is a framework for developing data flow
embedded systems on multiprocessor architecture. It allows to perform system-
level performance analysis and optimizing the mapping of software to hardware
architecture (processors, buses and memories). We have developed a compiler to
automatically translate DOL application into BIP models. We aim for building a
model of the application mapped to a specific hardware architecture by
transforming the BIP models we are getting in order to take into account the
constraints of the hardware platform.
Eduardo Mazza
Formal Methods and Software Liability
Abstract: The main objective of our work is to create a framework that
include the specification of the expected behaviour on individual
components as well as assumptions about their enviroment and a
liability relation associating commitments with identified agents. The
framework should also include techniques for the analysis of high
level execution traces to establish liabilities based on the formal
specification.
Polivios Pratikakis: Extending L2CA for the verification of
multi-threaded programs.
Abstract: L2CA is a tool for analyzing and verifying programs that
manipulate linked lists. Previously, L2CA focused on single-threaded
applications. Our current work focuses on extending L2CA to
multi-threaded programs with lock synchronization. I will talk about
L2CA, our extension to multi-threaded programs, and focus on the
problems that arise from parallelism, as well as our ideas on how to
solve them.
PIETREK Artur: Use of the LLVM framework for the MSIL code generation.
This presentation covers the MSIL (Microsoft .NET Intermediate
Language) code generation with the LLVM (Low Level Virtual Machine)
framework. While paying special attention to the C language input, the
generated MSIL code is intended to work correctly with the MONO .NET
implementation. The presentation describes shortly the MSIL, overviews
the LLVM framework and tells about current state of the MSIL code
generator, including things that are already implemented, problems
that need to be solved and their possible solutions.
KONECNY Filip: Software Verification Using Counter Automata
Abstract: In this talk, the aims of my thesis will be presented. The
talk will focus on latest work which concerns verification of integer
array programs and FLATA library, which is currently under
developpement and is intended to support verification of such
programs. In the approach to verification of array programs, arrays
are considered to be of finite, but not a priori bounded length. To
specify pre- and post-conditions, of programs, the SIL logic is
used. Effects of non-looping parts of code are computed syntactically
on the level of SIL. To compute the effect of a loop, the loop is
translated to a counter transducer and composed with a counter
automaton which corresponds to the loop precondition. The resulting
automaton is then converted back into SIL. Finally, validity of
user-specified postcondition can be checked as an entailment in SIL.
SIMACEK Jiri: Symbolic Verification of Pointer Programs using Tree Automata
Automated formal verification is a modern and rapidly evolving approach
to verifying correctness of computerized systems. There are, however,
still many problems that are to be solved to allow a really successful
application of formal verification methods in practice such as
verification of programs manipulating dynamic linked data structures
such as lists, trees, etc. We are trying to develop a new algorithm for
verification of such programs based on a symbolic representation of
heaps by finite tree automata. The approach uses an idea of splitting a
heap into seperate parts (inspired by the separation logic). Each part
of the heap is represented by a single automaton and these automata are
interconnected by special nodes called cutpoints.
PROCHNOW Steffen: Modeling systems based on semi-formal graphical formalism
Modeling systems based on semi-formal graphical formalisms, such as
Statecharts, has become standard practice in the design of reactive
embedded devices. Using paradigms established so far often results in
complex models that are difficult to comprehend and
maintain. Moreover, potential errors can be very subtle and hard to
locate in complex systems for the human beholder. This severely
compromises the practical use of the Statechart formalism.
To overcome this, a methodology to support the easy development and
understanding of complex Statecharts is presented. Central to this
approach is the usage of secondary notations to aid readability. For
the understanding of complex Statecharts during simulation a dynamic
focus-and-context view based on the semantics of Statecharts is
provided. As an alternative to the standard WYSIWYG editing paradigm,
which has some weaknesses for complex Statecharts, a graphical
approach is presented that is rather oriented towards the underlying
structure of the System Under Development, and another approach based
on a textual, dialect-independent Statechart description language. We
also present an approach to transform textual Esterel programs into
equivalent graphical Safe State Machines---a synchronous Statechart
variant. Furthermore, an approach analyzing Statecharts is focused
that limits or even prevents the use of error-prone expressions. An
empirical study on the usability and practicability of our Statechart
editing techniques, including a Statechart layout comparison,
indicates significant performance improvements in terms of editing
speed and model comprehension compared to traditional modeling
approaches. Furthermore, an outline of ongoing activities in the
SPEEDS project is given.
ABDELLATIF Tesnim: Real-Time Implementation of BIP
An embedded system is some combination of computer hardware and
software that is specifically designed for a particular kind of
application device. It generally interacts with an external
environment under physical constraints (deadlines, throughput, jitter,
power, processor, speed... ). Industrial machines, automobiles,
medical equipment, cameras, household appliances and airplanes as well
as the more obvious cellular phone are among the possible hosts of an
embedded system. The aim of our work is to study and develop
implementation techniques, meeting given quality of service
requirements. We can then implement embedded systems with respect of
their physical constraints. BIP is a unique component framework for
its expressiveness and adequacy for the description of heterogeneous
component-based systems. We can build descriptions of our systems
using BIP components to obtain faithful models. Those models can then
be verified either by using model checking techniques or by
application of specific structural analysis techniques to verify the
requirements. Our approach is to use those verified models, mostly
used for simulation, for implementation purpose. Modifications of the
execution engine of BIP with features supporting real-time execution
are then necessary. Indeed, the current BIP time advance is modeled
with logical time using global ticks synchronisations . Although it
can be interesting for modeling and simulation, nevertheless , it
stays inefficient for implementation. We introduce the notion of
real-time clock mapped to the platform's clock to compute the
real-time constraints. Real environment events are not taken into
account. Actually, the behavior of the environment is modeled for
simulation, it is predectible and totally controlled by the engine.
We introduce an event handler that handles those physical events. New
type of ports, “envports” are also introduceed to represent the
physical events in the model. The engine then maps the envports with
the physical events so as to deal with the real environment and still
benefit from the checks made over the model
Jacques Combaz : Real-Time Implementation of BIP : clocks and
real-time constraints.
Abstract:
In the current implementation of the BIP toolchain, timed
data are used to model local clocks. Time advance is achieved
synchronously by an implicit tick connector. Although this model can
be interesting for modeling and simulating systems, it cannot be used
in practice for implementation purposes. Using global tick
synchronizations often leads to inefficient implementations,
especially when the considered system is asynchronous.
Instead of simulating time by synchronizing every timed data
(i.e. local clock) with a global tick, we propose to introduce a
notion real-time clock and real-time constraint in the BIP programming
model. Clock synchronizations are not made explicitly by the user, but
are left to the Real-Time BIP Engine. We provide mechanisms for
computing real-time scheduling policies that meet the semantics of the
model.