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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26220%2F19%3APU134042" target="_blank" >RIV/00216305:26220/19:PU134042 - isvavai.cz</a>

Výsledek na webu

<a href="https://www.sciencedirect.com/science/article/pii/S240589631932693X" target="_blank" >https://www.sciencedirect.com/science/article/pii/S240589631932693X</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.ifacol.2019.12.744" target="_blank" >10.1016/j.ifacol.2019.12.744</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

20205 - Automation and control systems

Projekt

<a href="/cs/project/FV30037" target="_blank" >FV30037: Výzkum a vývoj nových řídicích systémů pro nákupní platformy.</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

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

ISBN

—

ISSN

2405-8963

e-ISSN

—

Počet stran výsledku

6

Strana od-do

127-132

Název nakladatele

Neuveden

Místo vydání

Neuveden

Místo konání akce

Tatranská lomnica

Datum konání akce

29. 10. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000507495200022