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 the environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the behaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited. In this paper we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex systems easier by providing a facility for automatically augmenting a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, that is, in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements. The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been implemented to automate the generation of artifacts that are typical of reliability analysis, for example fault trees. The platform can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the system model and of the possible faults. The interface of the platform has been designed to improve usability for people that are not expert in formal verification. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies.
The FSAP/NuSMV-SA Safety Analysis Platform
Bozzano, Marco;Villafiorita Monteleone, Adolfo
2007-01-01
Abstract
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 the environment. Such growing complexity requires an adequate increase in the capability of safety engineers to assess system safety, including analyzing the behaviour of a system in degraded situations. Formal verification techniques, like symbolic model checking, have the potential of dealing with such a complexity and are now being used more often. However, existing techniques have little tool support and therefore their use for safety analysis remains limited. In this paper we present FSAP/NuSMV-SA, a platform which aims to improve the development cycle of complex systems by providing a uniform environment that can be used both at design time and for safety assessment. The platform makes the modeling and safety assessment of complex systems easier by providing a facility for automatically augmenting a system model with failure modes, whose definitions are retrieved from a predefined library. In this way, it is possible to assess the system safety both in nominal conditions and in user-specified degraded situations, that is, in the presence of faults. Furthermore, the platform provides a pattern-based definition of temporal logic formulas, which simplifies the definition of safety requirements. The platform consists of a graphical user interface (FSAP) and an engine (NuSMV-SA) which is based on the NuSMV model checker. The model checking engine provides support for system simulation and standard model checking capabilities, like property verification and the generation of counterexamples. Furthermore, algorithms have been implemented to automate the generation of artifacts that are typical of reliability analysis, for example fault trees. The platform can derive fault trees automatically (for both monotonic and non-monotonic systems) from the definition of the system model and of the possible faults. The interface of the platform has been designed to improve usability for people that are not expert in formal verification. The platform has been evaluated in collaboration with an industrial partner and tested on some industrial case studies.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
