|
S‰minaire VASY 2010
|
|
Programme scientifique
|
Dimanche 20 Juin 2010 |
|
|
16h00 |
Arriv‰e |
|
|
DŽner |
|
Lundi 21 Juin 2010 |
|
|
9h00 |
Accueil et caf‰ |
|
10h00 – 11h00 |
Philippe Dhaussy et Amine Raji (ENSIETA) Contribution € la mise en œuvre de techniques de validation formelle de logiciels embarqu‰s
Cet expos‰, en deux parties, rend compte d’un travail s'inscrivant dans le cadre du d‰veloppement d'applications embarqu‰es pour lesquelles des phases de v‰rification formelle de modˆles logiciels sont n‰cessaires. Un d‰fi bien connu dans le domaine des m‰thodes formelles est d'am‰liorer leur int‰gration dans les processus de d‰veloppement industriel. Dans le contexte des systˆmes embarqu‰s, l’utilisation des techniques de v‰rification formelle de logiciels n‰cessitent tout d'abord de mod‰liser le systˆme € valider, puis de formaliser les propri‰t‰s devant Štre satisfaites sur le modˆle et enfin de d‰crire le comportement de l'environnement du modˆle. Ce dernier point que nous nommons ½ contexte de preuve © est souvent n‰glig‰. Il peut Štre, cependant, d'une grande importance afin de r‰duire la complexit‰ de la preuve. Dans notre contribution, nous cherchons € proposer € l’utilisateur une aide pour la formalisation de ce contexte en lien avec la formalisation des propri‰t‰s. Cette proposition vise € diminuer l'‰cart existant entre des modˆles de sp‰cification et des modˆles utilis‰s par des processus de model-checking en tirant parti de l'Ing‰nierie Dirig‰e par les Modˆles.
Dans une premiˆre partie, nous pr‰sentons un langage (DSL) que nous exp‰rimentons, nomm‰ CDL (Context Description Language), pour la description des acteurs de l’environnement, bas‰e sur des diagrammes d’activit‰s et de s‰quence et des patrons de d‰finition des propri‰t‰s € v‰rifier. Les modˆles d‰crits dans ce langage sont pris en charge par un outil prototype OBP (Observer-Based Prover) qui peut Štre connect‰ € des v‰rificateurs de type model-checker. Ces concepts ont ‰t‰ exp‰riment‰s sur plusieurs applications industrielles provenant de diff‰rents partenaires (Thales, Airbus, Cnes). Dans cet expos‰, nous rendons compte d’un retour d’exp‰rience et tirons les enseignements sur l’apport de cette approche, les difficult‰s d’appropriation du langage par les ing‰nieurs et limites rencontr‰es et donnons des perspectives de recherche et d‰veloppement.
Dans une deuxiˆme partie, et compte tenu du bilan tir‰ de nos exp‰rimentations industrielles, nous souhaitons explorer la possibilit‰ d’offrir un niveau de mod‰lisation des contextes plus proche des modˆles m‰tier manipul‰s dans les d‰veloppements industriels. L’id‰e est de consid‰rer CDL maintenant comme un format interm‰diaire pouvant Štre g‰n‰r‰ par des transformations de modˆle € partir des modˆles utilisateurs. La principale motivation derriˆre ce choix m‰thodologique consiste € offrir aux utilisateurs un mode de description des modˆles qu’ils ont l’habitude d’exercer. Toutefois, en regard de la nature h‰t‰rogˆne des modˆles utilis‰s par les utilisateurs dans le cadre de la mod‰lisation des systˆmes embarqu‰s, la g‰n‰ration automatique et complˆte de modˆles CDL n’est pas envisageable. En cons‰quence, nous proposons une approche semi-automatique bas‰e sur une g‰n‰ration en deux temps : L’utilisation d’un formalisme m‰tier pour d‰crire les modˆles de contextes et d’exigences € partir des modˆles d’analyse et de conception par le biais d’une adaptation manuelle, puis la g‰n‰ration automatique de modˆles CDL par des transformations de modˆles € partir des modˆles construits. Nous proposons que cette formalisation des contextes soit r‰alis‰e au sein de composants UCM (User Context Model) € partir d’une interpr‰tation d’exigences textuelles et d’une description de l’environnement du systˆme fourni par l’utilisateur. Des rˆgles de transformation sont € l’‰tude bas‰es sur les s‰mantiques formelles UCM et CDL. |
|
11h00 – 12h00 |
Hubert Garavel An Overview of CADP 2009 This lecture
will present the latest release of CADP (Construction and Analysis of
Distributed Processes), a toolbox for formal specification, verification, and
performance evaluation of concurrent systems. A new stable version of CADP is
scheduled to be released in the summer 2010. The major features of this new
version will be presented, with a special focus on the numerous enhancements
added between 2006 and 2010. |
|
|
D‰jeuner |
|
14h00 – 15h00 |
Vincent Powazny and Wendelin Serwe (joint work
with David Champelovier, Xavier Clerc, Hubert Garavel, Yves Guerte, Fr‰d‰ric
Lang, and Gideon Smeding) LOTOS NT and
its Translation to LOTOS In this
talk, we present the LOTOS NT language (version 5.0), a simplified
variant of the international standard E-LOTOS. In a nutshell, LOTOS NT
provides the same expressiveness as the international standard LOTOS, but
with more regular and user-friendly notations borrowed from imperative and
functional programming languages. In particular, the data type and process
parts of LOTOS NT share many similar constructs, leading to a more
uniform and easier-to-learn language than LOTOS. We present first the syntax
and static semantics of LOTOS NT. Then, we present its associated tools:
Lpp (a LOTOS NT preprocessor), Lnt2Lotos (a LOTOS NT to LOTOS
translator) and Lnt.Open (a interface with the
Open/C†sar framework enabling LOTOS NT specifications to be analyzed
using the CADP toolbox). |
|
15h00 – 15h30 |
Damien Thivolle (joint work with
Hubert Garavel) Verification of GALS
Systems by Combining Synchronous Languages and Process Calculi Synchronous languages
have been successful in designing safety-critical systems, e.g., in the
automotive and aeronautic industries. However, recent embedded systems
include an increasing amount of asynchrony that depart
from the synchronous-design assumptions used so far. Many of these systems
can be modelled using the GALS (Globally Asynchronous Locally Synchronous)
paradigm, i.e., a collection of sequential, deterministic components that
execute concurrently and communicate using slow or unreliable channels. We present a general
approach for modelling and verifying GALS systems
using a combination of synchronous languages (for the sequential components)
and process calculi (for communication channels and asynchronous
concurrency). This approach is illustrated with an industrial case-study
provided by Airbus: a TFTP/UDP communication protocol between a plane and the
ground, which is modelled using the Eclipse/TOPCASED workbench for
model-driven engineering and then analysed formally using the CADP
verification and performance evaluation toolbox. |
|
15h30 |
Pause caf‰ |
|
16h – 16h30 |
Fr‰d‰ric Lang Le langage interm‰diaire FIACRE
FIACRE (Format Interm‰diaire pour les Architectures de Composants R‰partis Embarqu‰s) est un langage con‡u dans le contexte des projets OpenEmbedd et Topcased, en collaboration avec les laboratoires LAAS-CNRS et IRIT. D‰riv‰ des modˆles NTIF et V-COTRE, Fiacre est destin‰ € servir de formalisme pivot entre les langages de mod‰lisation (tels que AADL) et les outils de v‰rification (tels que CADP et TINA). Nous pr‰sentons le langage FIACRE, ainsi que l'outil FLAC qui traduit automatiquement des modˆles FIACRE en modˆles LOTOS. |
|
16h30 – 17h00 |
Fr‰d‰ric Lang D‰monstrations : ‰tudes de cas a‰ronautique
Nous pr‰sentons deux cas du domaine de l'a‰ronautique (collaboration avec Airbus) qui ont ‰t‰ v‰rifi‰s avec CADP. Le premier est un protocole de transfert de fichiers (TFTP) utilis‰ dans les communications entre l'avion et le sol, d‰crit dans le langage SAM d'Airbus et traduit de maniˆre syst‰matique vers le langage LOTOS NT. Le second est une partie d'un systˆme de contrŸle de traffic a‰rien (ATC), d‰crit en Fiacre et traduit automatiquement vers le langage LOTOS en utilisant le traducteur FLAC. |
|
session confidentielle |
Simon Bouland Traduction de SDL vers LOTOS NT et application € l’‰tude de cas AFN
To be provided. |
|
|
DŽner |
|
Mardi 22 Juin 2010 |
|
|
9h00 – 9h30 |
Valentin Cristea (University
Polytehnica of Service oriented dependable distributed systems In this talk, we
present the current status of our research project on dependable systems,
which includes the formal verification of some components and of service
interaction protocols. The goal is to get feedback on this work and on
possible directions to continue the verification. |
|
9h30 – 10h15 |
Damien Thivolle (joint work with
Hubert Garavel) Verification of BPEL
2.0 web services with CADP Much has been published
in the scientific literature about the automated verification of Web
services, which is often done by taking Web services descriptions written in
BPEL (Business Processes Execution Language) and translating them into the
input formalism of some model checkers. However, most publications focus on
the behavioural aspects of BPEL, so that little information can be found on
how to handle the data types and expressions present in Web services
descriptions. This important issue is often neglected, as some approaches
cannot handle data aspects and abstract them away, and other approaches claim
to handle data but provide no detail. We address this issue
and propose a translation from BPEL to LOTOS NT, the most recent input
formalism for the CADP model checking toolbox. Considering the two standards
upon which BPEL is built (namely, XML Schema for data types, and XPath for
expressions), we focus on identifying the XML Schema and XPath subsets of
interest to Web services and defining an efficient translation of these
subsets into LOTOS NT. |
|
10h15 – 10h30 |
R‰mi H‰rilier Demonstration of the Contributor tool Contributor
allows a user to help the development of CADP by providing examples to enrich the regression test data-bases. |
|
10h30 |
Pause caf‰ |
|
11h00 – 12h00 |
Gwen Sala’n (joint work with
Olivier Gruber, Fabienne) Specifying and
Verifying the SYNERGY Apply Protocol with LOTOS-NT/CADP Synergy is a dynamic
reflexive system which is able to self-reconfigure. In this talk, we focus on
a part of this system, the apply protocol, which aims at reconfiguring an
architecture while supporting failures. We specified this protocol in
LOTOS-NT, and verified it using CADP verification tools. The experience was
successful because we have detected several issues which allowed to revise and correct several parts of the protocol. |
|
12h00 – 12h30 |
Alain Kaufmann Generating Test Data Using DGL The Data Generation
Language (DGL) offers a simple and efficient way to create data (test)
generators. Using a context-free grammar you will be able to generate test
patterns randomly, or exhaustively. This talk presents the basic concepts of
DGL and shows its usefulness through a few examples. |
|
|
D‰jeuner |
|
|
Aprˆs-midi libre |
|
|
DŽner |
|
Mercredi 23 Juin 2010 |
|
|
|
Holger Hermanns (Universit„t des Saarlandes and INRIA) When Interactive Markov Chains meet Probabilistic Automata (joint work with Christian Eisentraut and Lijun Zhang) We develop a
compositional behavioral model that integrates a variation of probabilistic
automata into a conservative extension of interactive Markov chains. The
model is rich enough to embody the semantics of generalized stochastic Petri
nets. We define strong and weak bisimulations and discuss their
compositionality properties. Weak bisimulation is partly oblivious to the
probabilistic branching structure, in order to reflect some natural equalities in this spectrum of models. As a result, the
standard way to associate a stochastic process to a generalized stochastic
Petri net can be proven sound with respect to weak bisimulation. |
|
9h45 – 10h45 |
Radu Mateescu and Wendelin Serwe A Study of
Shared-Memory Mutual Exclusion Protocols using CADP Mutual
exclusion protocols are an essential building block of concurrent systems:
indeed, such a protocol is required whenever a shared resource has to be
protected against concurrent non-atomic accesses. Hence, many variants of
mutual exclusion protocols exist in the shared-memory setting, such as
Peterson's or Dekker's well-known protocols. Although the functional
correctness of these protocols has been studied extensively, relatively
little attention has been paid to their non-functional aspects, such as their
performance in the long run. In this paper, we report on experiments with the
application of the Interactive Markov Chains approach to performance
evaluation of mutual exclusion protocols. Steady-state analysis provides an
additional criterion for comparing protocols, which complements the
verification of their functional properties. We also carefully re-examined
the functional properties, whose accurate formulation as temporal logic
formulas in the action-based setting turns out to be quite involved. |
|
10h45 |
Pause caf‰ |
|
|
Arnd Hartmanns (Universit„t des Saarlandes) Modelling and Model-Checking
with Modest Modest is a
compositional modelling formalism for stochastic timed systems. The language
allows the specification of real-time phenomena, probabilistic decisions (both
discrete and continuous) as well as a complex and dynamic process structure. Its
semantic model is a superset of well-known formalisms such as Timed Automata,
Markov Decision Processes and Probabilistic Timed Automata (PTA). I will
introduce the Modest language syntax and semantics, present an approach to
model-checking the subset of Modest corresponding to PTA, and, with the help
of one case study, give a short demonstration of our tools that support the
construction and analysis of Modest models.. |
|
|
D‰jeuner |
|
14h30 – 15h00 |
Iker Bellicot and Yann Genevois (joint work
with Jerome Fereyre, Hubert Garavel, R‰mi H‰rilier, Christophe Joubert, Radu
Mateescu, and Wendelin Serwe) Local resolution of
Boolean Equation systems and its applications to the analysis of state spaces To be provided. |
|
|
Jonathan Bogdoll (Universit„t des Saarlandes) Discrete Event Simulation for Modest in Practice Modest is a
compositional modeling formalism for stochastic timed systems. Model-checking
solutions are available for Modest, however, models
are sometimes inaccessible to model-checking due to their size. This gap is
bridged by simulation. Practical studies with our tool have shown that some
models of interest are nondeterministic, which makes them unsuitable for
simulation. Typical ways of removing nondeterminism are unsound, since model
output and behavior may be affected in unexpected ways. I will introduce
discrete event simulation and present a sound treatment of nondeterminism in
simulation. |
|
15h30 |
Pause caf‰ |
|
|
Pepijn Crouzen (Universit„t des Saarlandes) Aggregation Ordering for Massively
Compositional Models (joint work with Holger Hermanns) Compositional modeling
is a powerful way of expressing the behavior of a complex system through the
interaction of its components. Analysis of compositional models is difficult
because of the state space explosion. One solution is compositional
aggregation where composition and minimization steps are intertwined. This approach has proven
particularly useful in the area of compositional performance modeling.
However, one open question remains: in which order should the models be
composed, a question that is especially important for massively compositional
models derived automatically from higher level descriptions. Finding
the optimal composition ordering is generally infeasible, so heuristics are
necessary to find good orderings. In this paper we present a compositional
aggregation algorithm which harvests the heuristics suggested by Tai and
Koppol. Our algorithm takes into account the interaction between components,
the size of the component models and uses early elimination of bad
composition orders to dramatically decrease computation time. We show the
effectiveness of our algorithm by applying it
to randomly generated models as well as case studies from different
application areas. |
|
16h45 – 17h30 |
Fr‰d‰ric Lang Minimisation de graphes efficace avec l'outil Bcg_Min 2.0
Un aspect critique de la v‰rification bas‰e sur l'‰num‰ration des ‰tats est la maŽtrise de la taille du graphe des comportements. Les r‰ductions par bisimulation ont un moyen d'y parvenir. Depuis 2000, CADP inclut l'outil Bcg_Min qui impl‰mente les r‰ductions pour les bisimulations fortes et de branchement, ainsi que leurs variantes stochastiques et probabilistes. Dans cet expos‰, nous pr‰sentons une nouvelle version 2.0 de Bcg_Min, qui impl‰mente un algorithme bas‰ sur la notion de "signature" des ‰tats et am‰liore notablement les performances de la pr‰c‰dente version. |
|
17h30 |
ClŸture |