文章基本信息

标题：Design pattern for the runtime model-based checking of a real-time embedded system
本地全文：下载
作者：J. Arm ; Z. Bradac ; O. Bastan 等
期刊名称：IFAC PapersOnLine
印刷版ISSN：2405-8963
出版年度：2019
卷号：52
期号：27
页码：127-132
DOI：10.1016/j.ifacol.2019.12.744
语种：English
出版社：Elsevier
摘要：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.
关键词：KeywordsDesign patternsruntime verificationsafetydevice under testPetri netVHDL