Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks (2011)

AUTHORS:

ABSTRACT:

Safety instrumented systems (SIS) monitor industrial processes and automatically react on dangerous situations. SIS often consist of both logical and time-dependent building blocks. This paper introduces symbolic timed transition systems, a formalism designed for concise and modular description of SIS with clocks and similar time-dependent systems. Furthermore, an implementation of symbolic timed transition systems as an extension to NuSMV is devised. Two ways of checking properties on symbolic timed transition systems are developed: complete, region-abstraction-based model checking using binary decision diagrams and SMT-based bounded model

URL:
http://dx.doi.org/10.1109/ACSD.2011.29

@inproceedings{
    KJN11ACSD_ini,
    author = {Kindermann, Roland and Junttila, Tommi and Niemel{\"a}, Ilkka},
    publisher = "IEEE Computer Society",
    isbn = "978-0-7695-4387-1",
    language = "eng",
    title = "{Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks}",
    url = "http://dx.doi.org/10.1109/ACSD.2011.29",
    abstract = "Safety instrumented systems (SIS) monitor industrial processes and automatically react on dangerous situations. SIS often consist of both logical and time-dependent building blocks. This paper introduces symbolic timed transition systems, a formalism designed for concise and modular description of SIS with clocks and similar time-dependent systems. Furthermore, an implementation of symbolic timed transition systems as an extension to NuSMV is devised. Two ways of checking properties on symbolic timed transition systems are developed: complete, region-abstraction-based model checking using binary decision diagrams and SMT-based bounded model",
    corerank = "B",
    month = "June",
    responsibleauthor = {Kindermann, Roland and Junttila, Tommi and Niemel\"a, Ilkka},
    pages = "185-194",
    flags = "StMcDes HIIT copy",
    il = "no",
    year = "2011",
    keywords = "safety instrumented systems, symbolic model checking, NuSMV, region abstraction, timed systems",
    unitcode = "T306 =99, T312 = 1",
    impactfactor = "A4",
    booktitle = "{Proceedings of the 11th International Conference on Application of Concurrency to System Design, ACSD 2011}"
}

AUTHORS:

ABSTRACT:

URL: http://dx.doi.org/10.1109/ACSD.2011.29

URL:
http://dx.doi.org/10.1109/ACSD.2011.29