You are here

Roberto Cavada

Technologist
  • Phone: 0461314328
  • FBK Povo
Publications
  1. I. Pill; S. Semprini; R. Cavada; M. Roveri; R. Bloem; A. Cimatti,
    Formal analysis of hardware requirements,
    Proceedings of 43rd annual Design Automation Conference,
    New York, NY,
    2006
    , pp. 821-
    826
    , (DAC,
    San Francisco, USA,
    24/07/2006-28/07/2006)
  2. Marco Roveri; Alessandro Cimatti; Andrei Tchaltsev; Roberto Cavada; Simone Semprini; Roderick Bloem; Ingo Pill,
    2005,
  3. Alessandro Cimatti; Charles Pecheur; Roberto Cavada,
    Formal Verification of Diagnosability via Symbolic Model Checking,
    IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence,
    Morgan Kaufmann,
    2003
    , pp. 363-
    369
    , (IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence,
    Acapulco, Mexico,
    2003)
  4. 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
  5. Marco Roveri; Alessandro Cimatti; Roberto Cavada; Andrei Tchaltsev; Andrea Micheli; Alessandro Mariotti; Sergio Mover; Marco Pensallorto; Armando Tacchella; Daniel Sheridan; Gavin Keighren; Tommi Junttila; Timo Latvala,
    2002,

Pages