You are here

Publications

  1. 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 run-time) 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, real-world application. Symbolic model checking techniques are used to formally verify and check incrementally refine the diagnosability conditions,
    2003
  2. 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
  3. Alessandro Cimatti; Marco Pistore; Marco Roveri; Roberto Sebastiani,
    Improving the encoding of LTL Model Checking into SAT,
    VMCAI-2002 Workshop on Verification Model Checking and Abstract Interpretation,
    Springer,
    vol.2294,
    2002
    , pp. 196-
    207
    , (VMCAI-2002 Workshop on Verification Model Checking and Abstract Interpretation,
    2002)
  4. 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)
  5. Alessandro Cimatti; E. Giunchiglia; Marco Roveri; Marco Pistore; Roberto Sebastiani; A. Tacchella,
    Integrating BDD-based and SAT-based 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)
  6. 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)
  7. Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
    CADE-18 Conference on Automated Deduction,
    Springer,
    2002
    , pp. 195-
    210
    , (CADE-18 Conference on Automated Deduction,
    Copenhagen, Denmark,
    2002)
  8. Gilles Audemard; Piergiorgio Bertoli; Alessandro Cimatti; Artur Kornilowicz; Roberto Sebastiani,
    CALCULEMUS-2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
    2002
    , pp. 157-
    192
    , (CALCULEMUS-2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning,
    Marseille, France,
    2002)
  9. 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
  10. 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 Computer-Aided Verification,
    Springer,
    vol.2404,
    2002
    , pp. 359-
    364
    , (CAV 2002, Conference on Computer-Aided Verification,
    Copenhagen, Denmark,
    2002)

Pages