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

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

Paper in proceedings (conference paper)

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.

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.

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

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

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

2020

29.10.2019

16th IFAC Conference on Programmable Devices and Embedded Systems PDeS 2019

2405-8963

IFAC-PapersOnLine

2019

16

United Kingdom of Great Britain and Northern Ireland

127

132

6

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

http://hdl.handle.net/