Formal Methods and Discrete-Event Simulations

Aznam Yacoub (1) , Maamar El Amine Hamri (2, 1) , Claudia Frydman (2)

1 LIS - Laboratoire d'Informatique et Systèmes
2 MOFED - Modèles et Formalismes à Evénements Discrets

Les methodes formelles (FM) representent un formidable outil pour la Verification et la Validation (V&V) de logiciels et de systemes electroniques, voire de systemes au sens large, grace a l’emploi d’un raison- nement logique rigoureux. En particulier, les techniques dites de model-checking explorent de maniere exhaustive l’espace d’ etats de ces systemes et demontrent leur validite par rapport `a certaines specifications. Toutefois, ces techniques sont inefficaces, et mˆeme inapplicables sur des systemes complexes, tels que les syst`emes temporelles ou `a ́evenements discrets. A contrario, le domaine de la Modelisation et Simulation (M&S) fournit des outils et des techniques matures pour la V&V de ces systèmes. La mise au point d’un cadre de travail operationnel combinant FM et M&S semble alors etre une approche prometteuse permettant d’ameliorer qualitativement la V&V de modèles, et ainsi augmenter la confiance placee aux systemes etudiés ou conc ̧us. En particulier, nos travaux portent sur la combinaison entre SPIN, un outil reconnu de model-checking, et la simulation a evenements discrets pour la V&V de programmes.

Domains: Modeling and Simulation

Aznam Yacoub, Maamar El Amine Hamri, Claudia Frydman. Formal Methods and Discrete-Event Simulations. JDF 2016 - LES JOURNÉES DEVS FRANCOPHONES - THÉORIE ET APPLICATIONS, 2016, Cargèse, France. ⟨hal-03643337⟩