Publication detail

Design pattern for the runtime model-based checking of a real-time embedded system

ARM, J. BRADÁČ, Z. BAŠTÁN, O. STREIT, J. MIŠÍK, Š.

Original Title

Design pattern for the runtime model-based checking of a real-time embedded system

English Title

Design pattern for the runtime model-based checking of a real-time embedded system

Type

conference paper

Language

en

Original Abstract

As the safety requirements are becoming increasingly complex, methods and techniques to ensure testing and verification have to be optimized or even newly researched. Runtime verification thus appears to be more promising than offline statistical verification, which faces problems such state explosion and inefficient computational requirements. In this article, a runtime model-based checking monitor is described and implemented. This monitor utilizes the extended Petri net as the model, defined through formal semantics; the Petri net node is implemented by using VHDL. The monitor is assumed to run on an FPGA device connected to a device being tested. The Petri net model is the core of the designed monitor unit and embodies the design of a target application in the form of the design patterns. This approach exploits the model-based architecture concept and adds the runtime checking feature. The purpose of the proposed system is to detect errors such as deadlock, livelock, and starvation in a real-time embedded application. A wider goal or purpose then consists in making the monitor system ready to be incorporated into a fault-tolerant control system. Another goal then is to support the research concerning design patterns as the way to engineer or model safety-critical applications.

English abstract

As the safety requirements are becoming increasingly complex, methods and techniques to ensure testing and verification have to be optimized or even newly researched. Runtime verification thus appears to be more promising than offline statistical verification, which faces problems such state explosion and inefficient computational requirements. In this article, a runtime model-based checking monitor is described and implemented. This monitor utilizes the extended Petri net as the model, defined through formal semantics; the Petri net node is implemented by using VHDL. The monitor is assumed to run on an FPGA device connected to a device being tested. The Petri net model is the core of the designed monitor unit and embodies the design of a target application in the form of the design patterns. This approach exploits the model-based architecture concept and adds the runtime checking feature. The purpose of the proposed system is to detect errors such as deadlock, livelock, and starvation in a real-time embedded application. A wider goal or purpose then consists in making the monitor system ready to be incorporated into a fault-tolerant control system. Another goal then is to support the research concerning design patterns as the way to engineer or model safety-critical applications.

Keywords

Design patterns, runtime verification, safety, device under test, Petri net, VHDL

Released

29.10.2019

Pages from

127

Pages to

132

Pages count

6

URL

Documents

BibTex


@inproceedings{BUT159772,
  author="Jakub {Arm} and Zdeněk {Bradáč} and Ondřej {Baštán} and Jakub {Streit} and Štefan {Mišík}",
  title="Design pattern for the runtime model-based checking of a real-time embedded system",
  annote="As the safety requirements are becoming increasingly complex, methods and techniques to ensure testing and verification have to be optimized or even newly researched. Runtime verification thus appears to be more promising than offline statistical verification, which faces problems such state explosion and inefficient computational requirements. In this article, a runtime model-based checking monitor is described and implemented. This monitor utilizes the extended Petri net as the model, defined through formal semantics; the Petri net node is implemented by using VHDL. The monitor is assumed to run on an FPGA device connected to a device being tested. The Petri net model is the core of the designed monitor unit and embodies the design of a target application in the form of the design patterns. This approach exploits the model-based architecture concept and adds the runtime checking feature. The purpose of the proposed system is to detect errors such as deadlock, livelock, and starvation in a real-time embedded application. A wider goal or purpose then consists in making the monitor system ready to be incorporated into a fault-tolerant control system. Another goal then is to support the research concerning design patterns as the way to engineer or model safety-critical applications.",
  booktitle="16th IFAC Conference on Programmable Devices and Embedded Systems PDeS 2019",
  chapter="159772",
  doi="10.1016/j.ifacol.2019.12.744",
  howpublished="online",
  number="16",
  year="2019",
  month="october",
  pages="127--132",
  type="conference paper"
}