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

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Journal	Electronic Communications of the EASST
Volume	46
DOIs	https://doi.org/10.14279/tuj.eceasst.46.697.706
Publication status	Published - 1 Jan 2012
Externally published	Yes

Keywords

Altarica
Fault tree analysis
Model checking
Safety assessment

Access to Document

10.14279/tuj.eceasst.46.697.706

Cite this

@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

N1 - Publisher Copyright: © Automated Verification of Critical Systems 2011.

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

UR - https://www.scopus.com/pages/publications/84891883315

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

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this