La XXX° édition des journées FAC aura lieu les 2 et 3 avril 2025 à l’ISAE, en collaboration avec l’ONERA.

ISAE, 10 av. Edouard Belin 31055 Toulouse

bâtiment 61, amphithéâtre 4

(se présenter au poste de garde.)

Ces journées sont organisées par le groupe IFSE du RTRA STAE avec un soutien spécial de l’ENAC, l’INSA Toulouse, ISAE-Supaero, l’ONERA, Toulouse-INP et de l’Université Toulouse III, Paul Sabatier.

Si vous souhaitez participer, inscrivez-vous rapidement. La participation aux journées est gratuite, mais l’inscription est obligatoire.

Conférenciers invités

Cette année nos conférenciers invités sont:

  • Stefania Dumbrava (SAMOVAR et ENSIIE, équipe ACMES): Reliable Graph Data Processing at Scale: Challenges and Opportunities

Property graphs are widely used in applications handling interconnected, heterogeneous data, yet their schema definition remains less understood than in relational databases, posing challenges for data integrity. This talk first presents recent advances in specifying and discovering graph schema constraints and their role in improving database robustness. We then explore how schema-aware graph transformations can enhance the reliability of graph database applications, particularly through greybox fuzzing techniques that leverage code coverage feedback to generate more effective test inputs. Finally, we discuss key challenges in balancing availability, consistency, and constraint preservation at scale, highlighting open problems and future directions.

  • Frédéric Herbreteau (LaBRI et Bordeaux-INP, équipe MTV): Finite abstractions for the verification of (concurrent) timed automata

Timed automata are a commonly used model for verifying real-time systems. They extend finite automata by introducing clock variables, which allow for expressing constraints on the timing of events during a run. As these variables take values from non-negative real numbers, the state-space of timed automata is uncountably large. Formal verification algorithms use a finite symbolic representation of this state-space, called a zone graph. The finiteness of the zone graph is guaranteed through finite abstractions that preserve the properties being verified. We introduce the state-of-the-art abstraction, aLU, and demonstrate how it can be applied in verification algorithms in order to ensure termination.

In the second part, we focus on concurrent timed automata, where multiple timed processes (automata) interact with one another. In the typical global-time semantics, time progresses synchronously across all processes. We propose an alternative local-time semantics, where each process operates on its own timeline. We identify conditions under which the local-time semantics is equivalent to the global-time semantics. Additionally, we show that the local-time semantics has desirable properties, leading to a more compact state-space representation compared to the global-time approach. As with the global-time case, the finiteness of the zone graph in the local-time model relies on abstraction techniques. However, preserving certain properties is more complex in the local-time setting. We present solutions to adapt the aLU abstraction for use with local-time semantics.

À propos des journées FAC

La « formalisation des activités concurrentes » constitue un thème majeur de l’informatique, et fait l’objet de nombreux travaux de recherche et de développement, aussi bien au niveau national qu’international.

Au niveau local, ce thème est traité par le groupe de travail IFSE du RTRA STAE, et par les équipes de plusieurs laboratoires toulousains: IRIT-CNRS-UPS-INPT, LAAS-CNRS, ONERA.

Le groupe IFSE, précédemment groupe SVF de la fédération CNRS FéRIA, organise entre autres les journées FAC. Ces journées ont pour objet de présenter des travaux toulousains sur le thème de la « formalisation des activités concurrentes » : méthodes, techniques d’analyse, environnements logiciels reposant sur des bases formelles et assistant la spécification, la conception, le développement et la mise au point de systèmes réactifs, répartis et coopératifs, de réseaux de communication, de systèmes critiques…

À bientôt aux journées FAC.

Jean-Paul Bodeveix, Jean-Baptiste Raclet, Quentin Peyras, Marc Pantel, Philippe Quéinnec, Aurélie Hurault, Pascal Sotin, Iulian Ober, Christophe Garion, Célia Picard, David Chemouil, Pierre Roux, Nicolas Amat, Julien Brunel, Clément Foucher, Tomasz Kloda, Didier Le Botlan.