Symbolic model checking and safety assessment of Altarica models

Marco Bozzano; Alessandro Cimatti; Oleg Lisagor; Cristian Mattarei; Sergio Mover; Marco Roveri; Stefano Tonetta

doi:10.14279/tuj.eceasst.46.697.706

Symbolic model checking and safety assessment of Altarica models

Marco Bozzano
, Alessandro Cimatti
, Oleg Lisagor
, Cristian Mattarei
, Sergio Mover
, Marco Roveri
, Stefano Tonetta

Fondazione Bruno Kessler
University of York

Résultats de recherche: Contribution à un journal › Article › Revue par des pairs

Résumé

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.

langue originale	Anglais
journal	Electronic Communications of the EASST
Volume	46
Les DOIs	https://doi.org/10.14279/tuj.eceasst.46.697.706
état	Publié - 1 janv. 2012
Modification externe	Oui

Accès au document

10.14279/tuj.eceasst.46.697.706

Contient cette citation

@article{94f824b2da8542dca94ce3c05de883ce,

title = "Symbolic model checking and safety assessment of Altarica models",

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 tools.",

keywords = "Altarica, Fault tree analysis, Model checking, Safety assessment",

author = "Marco Bozzano and Alessandro Cimatti and Oleg Lisagor and Cristian Mattarei and Sergio Mover and Marco Roveri and Stefano Tonetta",

note = "Publisher Copyright: {\textcopyright} Automated Verification of Critical Systems 2011.",

year = "2012",

month = jan,

day = "1",

doi = "10.14279/tuj.eceasst.46.697.706",

language = "English",

volume = "46",

journal = "Electronic Communications of the EASST",

issn = "1863-2122",

}

TY - JOUR

T1 - Symbolic model checking and safety assessment of Altarica models

AU - Bozzano, Marco

AU - Cimatti, Alessandro

AU - Lisagor, Oleg

AU - Mattarei, Cristian

AU - Mover, Sergio

AU - Roveri, Marco

AU - Tonetta, Stefano

PY - 2012/1/1

Y1 - 2012/1/1

N2 - 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.

AB - 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.

KW - Altarica

KW - Fault tree analysis

KW - Model checking

KW - Safety assessment

U2 - 10.14279/tuj.eceasst.46.697.706

DO - 10.14279/tuj.eceasst.46.697.706

M3 - Article

AN - SCOPUS:84891883315

SN - 1863-2122

VL - 46

JO - Electronic Communications of the EASST

JF - Electronic Communications of the EASST

ER -

Symbolic model checking and safety assessment of Altarica models

Résumé

Accès au document

Empreinte digitale

Contient cette citation