
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 EuropeanUnionsponsored 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

Anna Perini; Marco Pistore; Marco Roveri; Angelo Susi,
Agentoriented modeling by interleaving formal and informal specification,
The goal of this paper is to discuss possibilities of intermixing 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 agentoriented 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

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)