An Organizing System to Perform and Enable Verification and Diagnosis Activities - Université de Bretagne Occidentale Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

An Organizing System to Perform and Enable Verification and Diagnosis Activities

Vincent Leilde
Vincent Ribaud

Résumé

Model-checkers increasing performance allows engineers to apply model-checking for the verification of real-life system but little attention has been paid to the methodology of model-checking. Verification " in the large " suffers of two practical problems: the verifier has to deal with many verification objects that have to be carefully managed and often re-verified; it is often difficult to judge whether the formalized problem statement is an adequate reflection of the actual problem. An organizing system-an intentionally arranged collection of resources and the interactions they support – makes easier the management of verification objects and supports reasoning interactions that facilitates diagnosis decisions. We discuss the design of such an organizing system , we show a straightforward implementation used within our research team. 1 Introduction System verification is used to establish that the design or product under consideration possesses certain properties. Formal verification has been advocated as a way forward to address verification tasks of complex embedded systems. Formal methods, within the field of computer science, is the formal treatment of problems related to the analysis of designs, but " it does not yet generally offer what its name seems to suggests, viz. methods for the application of formal techniques [1]. " Our research work is underlined by the observation that verification " in the large " causes a proliferation of interrelated models and verification sessions " that must be carefully managed in order to control the overall verification process [1]. " The main technique discussed in this paper is verification by model-checking. " Model checking is a formal verification technique which allows for desired behavioral properties of a given system to be verified on the basis of a suitable model of the system through systematic inspection of all states of the model [2]. " Model-checking walks through different phases within an iterative process [3]: modelling, running the model-checker and analyzing the results. Moreover, the entire verification should be planned, administered, and organized.
Fichier principal
Vignette du fichier
An Organizing System to Perform and Enable Verification and Diagnosis Activities.pdf (231.23 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01472718 , version 1 (21-02-2017)

Identifiants

  • HAL Id : hal-01472718 , version 1

Citer

Vincent Leilde, Vincent Ribaud, Philippe Dhaussy. An Organizing System to Perform and Enable Verification and Diagnosis Activities. Intelligent Data Engineering and Automated Learning – IDEAL 2016, Oct 2016, Yangzou, China. pp.576-587. ⟨hal-01472718⟩
478 Consultations
279 Téléchargements

Partager

Gmail Facebook X LinkedIn More