Séminaire VASY 2010
Corrençon-en-Vercors (Isère)

 

  


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
17h00 – 18h00

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 Bucharest)

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


9h00 – 9h45

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é


11
h15 – 12h15

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.


15h00 – 15h30

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é


16
h00 – 16h45

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