You are here

Publications

  1. Marco Bozzano; A. Cavallo; M. Cifaldi; L. Valacca; Adolfo Villafiorita,
    Improving Safety Assessment of Complex Systems: An Industrial case study,
    The complexity of embedded controllers is steadily increasing. This trend, stimulated by the continuous improvement of the computational power of hardware, demands for a corresponding increase in the capability of design and safety engineers to maintain adequate safety levels. The use of formal methods during system design has proved to be effective in several practical applications. The development of certain classes of applications, like, for instance, avionic system, however, also requires to analyse the behaviour of a system under certain degraded situations (e.g. when some components are not working as expected). This step, usually performed by safety engineers in a set of dedicated activities, has the goal of pointing out what are all the possible causes of a system malfunction or, more properly, a hazard of the system. It is an essential step to obtain the high safety levels required to keep public confidence in system behaviour, according to the current procedures for system certification (e.g., ARP4754). The integration of system design activities with safety assessment and the use of formal notations for the safety assessment of a system, although not new, are still at an early stage. These goals are addressed by the ESACS project, a European-Union-sponsored project grouping several industrial companies from the aeronautic field. The ESACS project is developing a methodology and a platform - the ESACS platform - that helps safety engineers automating certain phases of their work. An integral part of the project is the evaluation of the methodology and of the platform on a set of industrial case studies. This paper reports on the application of the ESACS methodology and on the use of the ESACS platform to one of such case studies, namely, the Secondary Power System of the Eurofighter Typhoon aircraft,
    2003
  2. Anna Perini; Marco Pistore; Marco Roveri; Angelo Susi,
    Agent-oriented modeling by interleaving formal and informal specification,
    The goal of this paper is to discuss possibilities of inter-mixing formal and informal specification in order to guide and support the conceptual modeling process in software development. We sketch a framework which rests on an agent-oriented methodology that provides a modeling language which allows for the definition of both informal and formal specification. We show how formal techniques can be used to guide and support the analyst while building and refining a conceptual model. Examples of its applications are discussed, with reference to the decision making process undertaken by the analyst when performing a set of activities relevant for requirements engineering, such as requirements elicitation and refinement, user validation of requirements specification, or management of requirements evolution. A case study taken from a technology transfer project in the agricultural domain is used to illustrate the approach,
    2003
  3. 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
  4. 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
  5. 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)
  6. 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)
  7. 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)
  8. 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)
  9. 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)
  10. 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)

Pages