
Alessandro Cimatti; C. Pecheur; Roberto Cavada,
Formal Verification of Diagnosability via Symbolic Model Checking,
This paper addresses the formal verification of diagnosis systems. We tackle the problem of diagnosability: given a partially observable dynamic system, and a diagnosis system observing its evolution over time, we discuss how to verify (at design time) if the diagnosis system will be able to infer (at runtime) the required information on the
hidden part of the dynamic state. We tackle the problem by looking for pairs of scenarios that are observationally indistinguishable, but lead to situations that are
required to be distinguished. We reduce the problem to a model checking problem. The finite state machine modeling the dynamic system is replicated to construct such pairs of scenarios; the diagnosability conditions are formally expressed in temporal logic; the check for diagnosability is carried out by solving a model checking problem. We ocus on the practical applicability of the method. We show how the formalism is adequate to represent diagnosability problems arising from a significant, realworld application. Symbolic model checking techniques are used to formally verify and check incrementally refine the diagnosability conditions,
2003

Bozzano, Marco; Delzanno, Giorgio; Martelli, Maurizio,
An effective fixpoint semantics for linear logic programs,
in «THEORY AND PRACTICE OF LOGIC PROGRAMMING»,
vol. 2,
n. 01,
2002
, pp. 85 
122

Alessandro Cimatti; Marco Pistore; Marco Roveri; Roberto Sebastiani,
Improving the encoding of LTL Model Checking into SAT,
VMCAI2002 Workshop on Verification Model Checking and Abstract Interpretation,
Springer,
vol.2294,
2002
, pp. 196
207
, (VMCAI2002 Workshop on Verification Model Checking and Abstract Interpretation,
2002)

Gilles Audemard; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
Bounded Model Checking for Timed Systems,
Formal Techniques for Networked and Distributed Systems  FORTE 2002. Proceedings of the 22nd IFIP TC6 WG 6.1 International Conference,
Springer,
2002
, pp. 243
259
, (Formal Techniques for Networked and Distributed Systems  FORTE 2002. Proceedings of the 22nd IFIP TC6 WG 6.1 International Conference,
Houston, Texas, USA,
2002)

Alessandro Cimatti; E. Giunchiglia; Marco Roveri; Marco Pistore; Roberto Sebastiani; A. Tacchella,
Integrating BDDbased and SATbased Symbolic Model Checking,
Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002,
Springer,
vol.2309,
2002
, pp. 49
56
, (Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002,
Santa Margherita Ligure, Italy,
2002)

Piergiorgio Bertoli; Alessandro Cimatti; J. Slaney; S. Thiebaux,
Solving Power Supply Restoration Problems with Planning via Symbolic Model Checking,
15th Eureopean Conference on Artificial Intelligence (ECAI 2002),
IOS Press,
2002
, pp. 576
580
, (15th Eureopean Conference on Artificial Intelligence (ECAI 2002),
Lyon, France,
2002)

Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
CADE18 Conference on Automated Deduction,
Springer,
2002
, pp. 195
210
, (CADE18 Conference on Automated Deduction,
Copenhagen, Denmark,
2002)

Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
CALCULEMUS2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
2002
, pp. 157
192
, (CALCULEMUS2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
Marseille, France,
2002)

Marco Bozzano; G. Delzanno,
Automated Protocol Verification in Linear Logic,
Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming [PPDP 2002],
2002

Alessandro Cimatti; E.M. Clarke; Enrico Giunchiglia; Fausto Giunchiglia; Marco Pistore; Marco Roveri; Roberto Sebastiani; A. Tacchella,
NuSMV 2: An OpenSource Tool for Symbolic model Checking,
CAV 2002, Conference on ComputerAided Verification,
Springer,
vol.2404,
2002
, pp. 359
364
, (CAV 2002, Conference on ComputerAided Verification,
Copenhagen, Denmark,
2002)