Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks

Reference:

Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks. In Proceedings of the 11th International Conference on Application of Concurrency to System Designg, ACSD 2011, pages 185–194. IEEE Computer Society, June 2011.

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

Keywords:

safety instrumented systems, symbolic model checking, NuSMV, region abstraction, timed systems

Suggested BibTeX entry:

@inproceedings{KJN11ACSD,
    author = {Roland Kindermann and Tommi Junttila and Ilkka Niemel{\"a}},
    booktitle = {{Proceedings of the 11th International Conference on Application of Concurrency to System Designg, ACSD 2011}},
    language = {eng},
    month = {June},
    pages = {185-194},
    publisher = {IEEE Computer Society},
    title = {{Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks}},
    year = {2011},
}