The FSAP/NuSMV-SA Safety Analysis Platform

摘要: Safety-critical systems are becoming more complex, both in the type of functionality they provide and way demanded to interact with environment. Such a growing complexity requires an adequate increase capability safety engineers assess system safety, including analyzing behavior degraded situations. Formal verification techniques, like symbolic model checking, have potential dealing such now being used often. However, existing techniques little tool support therefore their use for analysis remains limited. In this paper, we present FSAP/NuSMV-SA, platform which aims improve development cycle complex by providing uniform environment that can be at design time assessment. The makes modeling assessment easier facility automatically augmenting failure modes, whose definitions retrieved from predefined library. way, it is possible nominal conditions user-specified situations, i.e., presence faults. Furthermore, provides pattern-based definition temporal logic formulas, simplifies requirements. consists graphical user interface (FSAP) engine (NuSMV-SA) based on NuSMV checker. checking simulation standard capabilities, property generation counterexamples. algorithms been implemented automate artifacts typical reliability analysis, e.g., fault trees. derive trees (for monotonic non-monotonic systems) has designed usability people who not expert formal verification. evaluated collaboration industrial partner tested some case studies.