AltaRica is a language used to describe safety critical systems that has become a de-facto European industrial standard for Model-Based Safety Assessment (MBSA). However, even the most mature tool for the support for MBSA of AltaRica models, i.e. Dassault’s OCAS, has several limitations. The most important ones are its inability to perform many analyses exhaustively, severe scalability issues, and the lack of model checking techniques for temporal properties. In this paper we present a novel approach for the analysis of AltaRica models, based on a translation into an extended version of the model checker NuSMV. The translation relies on a novel formal characterization of the Dataflow dialect of AltaRica used in OCAS. The translation is formally defined, and its correctness is proved. Based on this formal characterization, a toolset has been developed and integrated within OCAS, thus enabling functional verification and safety assessment with the state of the art techniques of NuSMV. The whole approach is validated by an experimental evaluation on a set of industrial case studies, which demonstrates the advantages of the proposed technique over the currently available tools.
Safety Assessment of AltaRica Models via Symbolic Model Checking
Bozzano, Marco;Cimatti, Alessandro;Mattarei, Cristian;Mover, Sergio;Roveri, Marco;Tonetta, Stefano
2015-01-01
Abstract
AltaRica is a language used to describe safety critical systems that has become a de-facto European industrial standard for Model-Based Safety Assessment (MBSA). However, even the most mature tool for the support for MBSA of AltaRica models, i.e. Dassault’s OCAS, has several limitations. The most important ones are its inability to perform many analyses exhaustively, severe scalability issues, and the lack of model checking techniques for temporal properties. In this paper we present a novel approach for the analysis of AltaRica models, based on a translation into an extended version of the model checker NuSMV. The translation relies on a novel formal characterization of the Dataflow dialect of AltaRica used in OCAS. The translation is formally defined, and its correctness is proved. Based on this formal characterization, a toolset has been developed and integrated within OCAS, thus enabling functional verification and safety assessment with the state of the art techniques of NuSMV. The whole approach is validated by an experimental evaluation on a set of industrial case studies, which demonstrates the advantages of the proposed technique over the currently available tools.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
