An Organizing System to Perform and Enable Verification and Diagnosis Activities

Vincent Leilde 1 Vincent Ribaud 2 Philippe Dhaussy 1
1 Lab-STICC_ENSTAB_CACS_MOCS ; IDM
STIC - Pôle STIC [Brest], Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance
2 Lab-STICC_UBO_CACS_MOCS
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance, UBO - Université de Brest
Abstract : 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.
Type de document :
Communication dans un congrès
Intelligent Data Engineering and Automated Learning – IDEAL 2016, Oct 2016, Yangzou, China. Lectune Notes in Computer Science (9937), pp.576-587, 2016, Proceedings of the 17th International Conference on Intelligent Data Engineering and Automated Learning – IDEAL 2016. 〈http://www.springer.com/fr/book/9783319462561#〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

http://hal.univ-brest.fr/hal-01472718
Contributeur : Vincent Ribaud <>
Soumis le : mardi 21 février 2017 - 11:16:02
Dernière modification le : mardi 16 janvier 2018 - 15:54:24
Document(s) archivé(s) le : lundi 22 mai 2017 - 14:33:27

Fichier

An Organizing System to Perfor...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01472718, version 1

Citation

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. Lectune Notes in Computer Science (9937), pp.576-587, 2016, Proceedings of the 17th International Conference on Intelligent Data Engineering and Automated Learning – IDEAL 2016. 〈http://www.springer.com/fr/book/9783319462561#〉. 〈hal-01472718〉

Partager

Métriques

Consultations de la notice

295

Téléchargements de fichiers

73