Challenges in Embedded Model Checking - A Simulator for the [mc]square Model Checker

被引：4

作者：

Reinbacher, Thomas ^{[1
]}

Kramer, Michael ^{[1
]}

Horauer, Martin ^{[1
]}

Schlich, Bastian ^{[2
]}

机构：

[1] Univ Appl Sci Technikum Wien, Inst Embedded Syst, Hochstadtpl 5, A-1200 Vienna, Austria

[2] Rhein Westfal TH Aachen Univ, Embedded Software Lab Informat 11, D-52074 Aachen, Germany

来源：

2008 INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS | 2008年

关键词：

D O I：

10.1109/SIES.2008.4577709

中图分类号：

T [工业技术];

学科分类号：

08 ;

摘要：

Model checking is considered a promising approach for the verification of software for embedded systems. Generating system models that are close to real-life behavior, however, h challenging. As a result, in some approaches a model can be is automatically constructed out of the assembly code along with an appropriate target simulator/debugger. The implementation of the latter is crucial for the entire verification process. To that end, this paper presents requirements and challenges that arise when implementing and verifying such a simulator for the [mc]square model checker from the RWTH Aachen University.

引用

页码：245 / +

页数：2

共 50 条

[41] The JKIND Model Checker [J].

Gacek, Andrew ;

Backes, John ;

Whalen, Mike ;

Wagner, Lucas ;

Ghassabani, Elaheh .

COMPUTER AIDED VERIFICATION, CAV 2018, PT II, 2018, 10982 :20-27

[42] The SPINJA Model Checker [J].

de Jonge, Marc ;

Ruys, Theo C. .

MODEL CHECKING SOFTWARE, 2010, 6349 :124-128

[43] Development of SMT-Based Bounded Model Checker for Embedded Assembly Program [J].

Kobashi, Jumpei ;

Yamane, Satoshi ;

Takeshita, Atsushi .

2014 IEEE 3RD GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE), 2014, :696-698

[44] COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking [J].

Gross, Dennis ;

Jansen, Nils ;

Junges, Sebastian ;

Perez, Guillermo A. .

DEPENDABLE SOFTWARE ENGINEERING. THEORIES, TOOLS, AND APPLICATIONS, SETTA, 2022, 13649 :41-49

[45] Generating MC/DC adequate test sequences through model checking [J].

Rayadurgam, S ;

Heimdahl, MPE .

28TH ANNUAL NASA GODDARD SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS, 2004, :91-96

[46] Generic Model Checking for Modal Fixpoint Logics in COOL-MC [J].

Hausmann, Daniel ;

Humml, Merlin ;

Prucker, Simon ;

Schroeder, Lutz ;

Strahlberger, Aaron .

VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT I, 2024, 14499 :171-185

[47] Model checking deep neural networks: opportunities and challenges [J].

Sbai, Zohra .

FRONTIERS IN COMPUTER SCIENCE, 2025, 7

[48] Statistical Model Checking of Approximate Circuits: Challenges and Opportunities [J].

Strnadel, Josef .

PROCEEDINGS OF THE 2020 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE 2020), 2020, :1574-1577

[49] Spatial Model Checking for Smart Stations Research Challenges [J].

ter Beek, Maurice H. ;

Ciancia, Vincenzo ;

Latella, Diego ;

Massink, Mieke ;

Spagnolo, Giorgio O. .

FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2021, 2021, 12863 :39-47

[50] Delayed nondeterminism in model checking embedded systems assembly code [J].

Noll, Thomas ;

Schlich, Bastian .

HARDWARE AND SOFTWARE: VERIFICATION AND TESTING, 2008, 4899 :185-201

← 1 2 3 4 5 →