Altarica is a language used to describe critical systems. In this paper we present a novel approach to the analysis of Altarica models, based on a translation into an extended version of NuSMV. This approach opens up the possibility to carry out functional verification and safety assessment with symbolic techniques. An experimental evaluation on a set of industrial case studies demonstrates the advantages of the approach over currently available tools
Model Checking and Safety Assessment of Altarica models / Bozzano, M.; Cimatti, A.; Lisagor, O.; Mattarei, C.; Mover, S.; Roveri, M.; Tonetta, S.. - In: ELECTRONIC COMMUNICATIONS OF THE EASST. - ISSN 1863-2122. - 46:(2011). (Intervento presentato al convegno AVOCS 2011 - 11th International Workshop on Automated Verification of Critical Systems tenutosi a Newcastle, UK nel da 09/12/2011 a 09/14/2011).
Model Checking and Safety Assessment of Altarica models
A. Cimatti;C. Mattarei;S. Mover;M. Roveri;S. Tonetta
2011-01-01
Abstract
Altarica is a language used to describe critical systems. In this paper we present a novel approach to the analysis of Altarica models, based on a translation into an extended version of NuSMV. This approach opens up the possibility to carry out functional verification and safety assessment with symbolic techniques. An experimental evaluation on a set of industrial case studies demonstrates the advantages of the approach over currently available toolsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
