You are here

2003

  1. Marco Bozzano; Adolfo Villafiorita,
    Improving System Reliability via Model Checking: the FSAP/NuSMV-SA Safety Analysis Platform,
    Computer Safety, Reliability, and Security. Proceedings of the 22nd International Confecence SAFECOMP 2003,
    2003
    , pp. 49-
    62
    , (Computer Safety, Reliability, and Security. Proceedings of the 22nd International Confecence SAFECOMP 2003,
    2003)
  2. Marco Bozzano; A. Cavallo; M. Cifaldi; L. Valacca; Adolfo Villafiorita,
    Improving Safety Assessment of Complex Systems: An Industrial case study,
    FME 2003: Formal Methods. Proceedings of the International Symposium of Formal Methods,
    2003
    , pp. 208-
    222
    , (FME 2003: Formal Methods. Proceedings of the International Symposium of Formal Methods,
    2003)
  3. Marco Benedetti; Alessandro Cimatti,
    Bounded Model Checking for past LTL,
    Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 9th International Conference, TACAS 2003,
    Springer,
    vol.2619,
    2003
    , pp. 18-
    33
    , (Tools and Algorithms for the Construction and Analysis of Systems. Proceedings of the 9th International Conference, TACAS 2003,
    2003)
  4. 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)
  5. Gilles Audemard; Marco Bozzano; Alessandro Cimatti; Roberto Sebastiani,
    CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
    2003
    , pp. 62-
    76
    , (CADE-19 Workshop: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR`03),
    Miami, USA,
    2003)
  6. A. Fuxman; L. Liu; Marco Pistore; Marco Roveri; John Mylopoulos,
    Specifying and Analyzing Early Requirements: Some Experimental Results,
    Formal Tropos is a specification language for early requirements. It is based on concepts from an agent-oriented early requirement model framework (i*) and extends them with a rich temporal specification language. In earlier work, we demonstrated through a small case study how model checking could be used to verify early requirements written in Formal Tropos. In this paper we address issues of methodology and scalability for our earlier proposal. In particular, we propose guidelines for producing a Formal Tropos specification from an i* diagram and for deciding what model checking technique to use when a particular formal property is to be validated. We also evaluate the scope and scalability of our proposal using a tool, the T-Tool, that maps Formal Tropos specifications to a language that can be handled by NuSMV, a state-of-the-art model checker. Our experiments are based on a course management case study,
    2003
  7. Piergiorgio Bertoli; Alessandro Cimatti; Lago U. Dal; Marco Pistore,
    Extending PDDL to mondeterminism, limited sensing and iterative conditional plans,
    The last decade has witnessed a dramatic progress in the variety and performance of techniques and tools for classical planning. Much of this can be ascribed to the existence of a de-facto standard modeling language for classical planning, PDDL. PDDL has fostered information sharing and data exchange in the planning community, and has made international classical planning competitions possible. At the same time, in the last few years, non-classical planning has gained considerable attention, due to its capability to capture relevant features of real-life domains which the classical framework fails to express. However, no significant effort has been made to achieve a standard means for expressing non-classical problems, making it difficult for the planning community to compare non-classical approaches and systems. This paper provides a contribution in this direction. We extend PDDL in order to express three very relevant features outside classical planning: uncertainty in the initial state, nondeterministic actions, and partial observability. NPDDL's extensions are designed to retain backward compatibility with PDDL, and with an emphasis on compactness of the representation. Moreover, we define a powerful, user-friendly plan language to go together with NPDDL. The language allows expressing program-like plans with branching and iterations structures, as it is necessary to solve planning problems in the presence of initial state uncertainty, nondeterminism and partial observability. We are testing NPDDL's ability to cope with a variety of problems, as they are handled by a state-of-the-art planner, MBP,
    2003
  8. Marco Bozzano; Adolfo Villafiorita,
    Improving System Reliability via Mdel Checking: the FSAP/NuSMV-SA Safety Analysis Platform,
    Safety critical systems are becoming more complex, both in the type of functionality they provide and in the way they are demanded to interact with their environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the bahaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are more often being used during system design. In this paper we present the FSAP/NuSMV-SA platform, based on the NuSMV2 model checker, that implements known and novel techniques to help safety engineers perform safety analysis. The main functionality of FSAP/NuSMV-SA include: failure mode definition based on a library of failure modes, fault injection, automatic fault tree construction for monotonic and non-monotonic systems, failure ordering analysis. The goal is to provide an environment that can be used both by design engineers to formally verify a system and by safety engineers to automate certain phases of safety assessment. The platform is being developed within the ESACS project (Enhanced Safety Analysis for Complex Systems), an European-Union-sponsored project in the avionics sector, whose goal is to define a methodology to improve the safety analysis practice for complex systems development,
    2003
  9. 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
  10. 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

Pages