Deductive Verification of Parameterized Embedded Systems Modeled in SystemC

Philip Tasche*, Raúl E. Monti, Stefanie Eva Drerup, Pauline Blohm, Paula Herber, Marieke Huisman

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Major strengths of deductive verification include modular verification and support for functional properties and unbounded parameters. However, in embedded systems, crucial safety properties often depend on concurrent process interactions, events, and time. Such properties are global in nature and thus difficult to verify in a modular fashion. Furthermore, the execution and scheduling semantics of industrially used embedded system design languages such as SystemC are typically only informally defined. In this paper, we propose a deductive verification approach for embedded systems that are modeled with SystemC. Our main contribution is twofold: 1) We provide a formal encoding and an automated transformation of SystemC designs for verification with the VerCors deductive verifier. 2) We present a novel approach for invariant construction to abstractly capture global dependencies. Our encoding enables an automated formalization and deductive verification of parameterized SystemC designs, and the invariant construction enables local reasoning about global properties with comparatively low manual effort. We demonstrate the applicability of our approach on three parameterized case studies, including an automotive control system.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
Subtitle of host publication25th International Conference, VMCAI 2024 London, United Kingdom, January 15–16, 2024 Proceedings, Part II
EditorsRayna Dimitrova, Ori Lahav, Sebastian Wolff
PublisherSpringer
Pages187-209
Number of pages23
ISBN (Electronic)978-3-031-50521-8
ISBN (Print)78-3-031-50520-1
DOIs
Publication statusPublished - 2024
Event25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024 - London, United Kingdom
Duration: 15 Jan 202416 Jan 2024
Conference number: 25

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14500 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024
Abbreviated titleVMCAI 2024
Country/TerritoryUnited Kingdom
CityLondon
Period15/01/2416/01/24
Otherco-located with 51st ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2024

Keywords

  • 2024 OA procedure

Fingerprint

Dive into the research topics of 'Deductive Verification of Parameterized Embedded Systems Modeled in SystemC'. Together they form a unique fingerprint.

Cite this