Ces journées ont été organisées par le groupe IFSE du RTRA STAE.

Les journées FAC'2015 ont eu lieu les 22 et 23 avril 2015 à IRIT - SITE ENSEEIHT (SALLE DES THÈSES, C002).

Programme des journées :

Mercredi 22 avril

  • 9h00 : accueil

  • 9h30-10h30 : Ahmed Bouajjani Paris 7, LIAFA : Verification of Concurrent Programs: Decidability, Complexity, Reductions.

abstract:

Concurrency is omnipresent in computer systems, at all levels, from applications relying on high level synchronization mechanisms and using abstract data structures, to low level code implementing concurrent/distributed data structures and system services over multi-core architectures/large-scale networks. The automated verification of concurrent programs is a challenging problem due to their highly complex behaviours.

We will address the problem of verifying automatically concurrent programs, from the point of view of decidability and complexity. We will show the difficulties that raise in addressing this problem in different contexts: shared-memory, message passing, dynamic creation of tasks, recursion, relaxed memory models, etc. We will overview existing approaches for handling these issues, and we will show in particular how verification problems for concurrent programs can be reduced to ”simpler” problems (stated as reachability queries either on sequential programs, or on concurrent but sequentially consistent programs) for which there are already know verification algorithms and tools.

  • 10h30-11h00 : pause

  • 11h00-12h30 : logique et automate

    • Regular Sensing.   () S. Almagor, D. Kuperberg, O. Kupferman

    • Quotient of Acceptance Specifications under Reachability Constraints.   () G. Verdier, J.-B. Raclet

    • On Finite Domains in First-Order Linear Temporal Logic. J. Brunel, D. Chemouil, D. Kuperberg

  • 12h30-14h00 : déjeuner

  • 14h00-15h30 : preuve

    • Büchi Automata Optimisations Formalised in Isabelle/HOL.   () A. Schimpf, J.-G. Smaus

    • Provably correct graph transformations with small-tALC. N. Baklanova, J. H. Brenas, R. Echahed, C. Percebois, M. Strecker, Hanh Nhi Tran

    • Formal Proofs of Rounding Error Bounds.

P. Roux

  • 15h30-16h00 : pause

  • 16h00-17h00 : analyse de sûreté de fonctionnement

    • Building System Awareness: Cache Characterization through Probabilities. N. Gobillot, A. Melani, F. Guet, L. Santinelli, E. Noulard, D. Doose, C. Lesire-Cabaniols, J. Morio

    • Automatic architecture hardening using safety patterns.

K. Delmas, R. Delmas, C. Pagetti

Jeudi 23 avril

abstract:

Model-based design (MBD) is a design methodology that relies on three key elements: modeling (how to capture the system that we want), analysis (how to be sure that this is the system that we want before actually building it), and synthesis (how to build the system). In this talk I will present some recent work on two aspects of MBD: synthesis and compositionality. I will first present synthesis of distributed control protocols from scenarios and requirements. Automated synthesis of such protocols is a hard, generally undecidable, problem. Nevertheless, by allowing the designer to specify, in addition to a set of formal requirements, a set of example scenarios that illustrate how the protocol should behave in certain situations, we are able to fully automatically synthesize several simple distributed protocols.

I will then discuss compositional methods, which allow to build systems from smaller components. Such methods are not simply a desirable feature in system design: they are a must for building large and complex systems. A key ingredient for compositionality is that of an “interface”. An interface abstracts a component, exposing relevant information while hiding internal details. I will give an overview of the many uses of interfaces in MBD, from modular code generation from hierarchical models, to incremental design with interface theories, to co-simulation and multiview modeling.

  • 10h30-11h00 : pause

  • 11h00-12h30 : modélisation et véfication formelles

    • Formal Modelling and Verification of Cooperative Ant Behaviour in Event-B.   () L. Laibinis, E. Troubitsyna, Z. Graja, F. Migeon, A. H. Kacem

    • A formal encoding for Petri nets in Agda. M. Montin

    • A Framework for the Verification of Asynchronously Communicating Services.

F. Chevrou, A. Hurault, P. Mauran, P. Quéinnec, X. Thirioux

  • 12h30-14h00 : déjeuner

  • 14h00-15h30 : temps-réel

    • Time Petri Nets with Dynamic Firing Dates: Semantics and Applications.   () B. Berthomieu, S. Dal-Zilio, L. Fronc, F. Vernadat

    • SimSo: A Simulation Tool to Evaluate Real-Time Multiprocessor Scheduling Algorithms.   () M. Chéramy, P.-E. Hladik, A.-M. Déplanche

    • Model-Checking Real-Time Properties of an Auto Flight Control System Function.   () P.-A. Bourdil, B. Berthomieu, E. Jenn

  • 15h30-16h00 : pause

  • 16h00-17h00 :

    • Binding Structures as an Abstract Data Type (revisited).   () W. Ricciotti

    • Parameterizing the concurrency of a concurrency-aware eXecutable Domain-Specific Modeling Language with runtime domain data in a decoupled manner.

F. Latombe, X. Crégut, B. Combemale, J. De Antoni and M. Pantel