Projets-App
Projets
Editer un projet
Cadre de travail
Unité de recherche rattachée au CNRS
IRIF
LIPN
LMF
Information du ou de la responsable scientifique du projet :
Prénom
Nom
E-mail
Présentation du projet scientifique
Nom du project
Résumé publiable du projet (10 lignes max.)
We have recently shown how rewriting-modulo-SMT can be an appropriate semantic framework for the specification and verification of real-time systems. Applications include the definition of interpreters for Parametric Timed Automata and Parametric Time Petri Nets. The results are promising and the implementation of the rewrite theories in Maude show that our methods can be used in practice, outperforming in some cases state-of-the-art tools in the field. The analysis of real-time system in Maude requires the definition of a folding procedure for guaranteeing termination when the parametric zone graph is finite. Such a procedure checks when two symbolic states, possibly syntactical different, define the same set of concrete states. This project aims at improving the efficiency of our rewrite tools by implementing, at the C++ level of Maude, a general folding procedure to guarantee termination. Currently, this procedure is implemented at the meta-level of Maude.
Champs thématiques adressés (séparés par des virgules)
Type
proof-of-concept
prototype
maintenance/évolution logiciel existant
prématuration
Décrivez les innovations attendues à l'issue du projet (5 lignes max.)
Faster procedures in rewriting logic and Maude for the analysis of real-time systems.
Argumentaire scientifique qui décrit le projet, l'état de l'art, les travaux antérieurs et les résultats attendus (20 lignes max.)
Our works [1] and [2] have opened a new avenue for the use of rewriting modulo SMT techniques for the analysis of real-time systems specified as parametric timed automata or time Petri nets. The use of SMT in the context of rewriting solves the problem of rewriting rules with extra variables on the right hand side. Those variables are handled by the SMT solver, constrained by boolean expressions in the rewrite rule. Hence, it is possible to symbolically express delay transitions where the actual time is not fixed but constrained, e.g., by conditions in guards and invariants in states. The new extra SMT variables pose a problem: at each transition, fresh variables are created and equivalent symbolic states are not necessarily syntactically equal. Therefore, the search procedures in Maude cannot detect when the (symbolic) state has been already visited and stop exploring such a state. For solving the above mentioned problem, we have proposed folding techniques that guarantee termination under certain conditions. Such methods have been implemented at the meta-level of Maude, thus incurring in extra overloads. This project aims at implementing the folding procedures at the C++ level of Maude, hence improving the efficiency of the tools we have proposed. [1] Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci, Fredrik Rømming: Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata. FTSCS 2022: 3-15 [2] Jaime Arias, Kyungmin Bae, Carlos Olarte, Peter Csaba Ölveczky, Laure Petrucci, Fredrik Rømming: Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving. Petri Nets 2023: 369-392
Description du besoin en ingénierie
Évaluez le temps ingénieur dont vous avez besoin pour votre projet:
Frequence
2 jour/semaine
3 jour/semaine
Durée
1 mois
2 mois
3 mois
4 mois
5 mois
6 mois
Quelles sont les compétences spécifiques d'ingénierie attendues ; notamment, langages ou frameworks qui seront utilisés dans le projet, outils existants, connaissances requises ?
Experience in SMT solvers and C++.
Décrivez les activités qui seront confiées à·aux ingénieur·e·s (si possible, avec un planning de tâches attendues)
1. Knowing the interface of Maude with SMT solvers 2. Exploring the source code of Maude 3. Implement the new search procedure with folding
Commentaires
Mettre à jour