Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks (2011)
AUTHORS:
Kindermann Roland
,
Junttila Tommi
,
Niemelä Ilkka
BOOKTITLE:
Proceedings of the 11th International Conference on Application of Concurrency to System Design, ACSD 2011
PAGES:
185-194
URL:
http://dx.doi.org/10.1109/ACSD.2011.29
@inproceedings{ KJN11ACSD, 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}, 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}", pages = "185-194" }