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

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/244820
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact