An organizing system to perform and enable verification and diagnosis activities

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.