HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

An Organizing System to Perform and Enable Verification and Diagnosis Activities

Vincent Leilde 1 Vincent Ribaud 2 Philippe Dhaussy 1
Lab-STICC - Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (UMR 3192)
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

Contributor : Vincent Ribaud Connect in order to contact the contributor
Submitted on : Tuesday, February 21, 2017 - 11:16:02 AM
Last modification on : Monday, March 14, 2022 - 11:08:08 AM
Long-term archiving on: : Monday, May 22, 2017 - 2:33:27 PM


An Organizing System to Perfor...
Files produced by the author(s)


  • HAL Id : hal-01472718, version 1


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⟩



Record views


Files downloads