Formal Methods and Discrete-Event Simulations

International audienceLes methodes formelles (FM) representent unformidable outil pour la Verification et la Validation(V&V) de logiciels et de systemes electroniques, voirede systemes au sens large, grace a l’emploi d’un raison-nement logique rigoureux. En particulier, les techniquesdites de model-checking explorent de maniere exhaustivel’espace d’ etats de ces systemes et demontrent leurvalidite par rapport `a certaines specifications. Toutefois,ces techniques sont inefficaces, et mˆeme inapplicablessur des systemes complexes, tels que les syst`emestemporelles ou `a ́evenements discrets. A contrario,le domaine de la Modelisation et Simulation (M&S)fournit des outils et des techniques matures pour laV&V de ces systèmes. La mise au point d’un cadre detravail operationnel combinant FM et M&S semble alorsetre une approche prometteuse permettant d’ameliorerqualitativement la V&V de modèles, et ainsi augmenterla confiance placee aux systemes etudiés ou conc ̧us.En particulier, nos travaux portent sur la combinaisonentre SPIN, un outil reconnu de model-checking, etla simulation a evenements discrets pour la V&V deprogrammes