Detail publikace

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, Š.

Originální název

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

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Vydáno

29. 10. 2019

ISSN

2405-8963

Periodikum

IFAC-PapersOnLine (ELSEVIER)

Ročník

2019

Číslo

16

Stát

Nizozemsko

Strany od

127

Strany do

132

Strany počet

6

URL

https://www.sciencedirect.com/science/article/pii/S240589631932693X

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",
  booktitle="16th IFAC Conference on Programmable Devices and Embedded Systems PDeS 2019",
  year="2019",
  journal="IFAC-PapersOnLine (ELSEVIER)",
  volume="2019",
  number="16",
  pages="127--132",
  doi="10.1016/j.ifacol.2019.12.744",
  issn="2405-8963",
  url="https://www.sciencedirect.com/science/article/pii/S240589631932693X"
}