@InProceedings{Tasche24,
author="Tasche, Philip
and Monti, Ra{\'u}l E.
and Drerup, Stefanie Eva
and Blohm, Pauline
and Herber, Paula
and Huisman, Marieke",
editor="Dimitrova, Rayna
and Lahav, Ori
and Wolff, Sebastian",
title="Deductive Verification of Parameterized Embedded Systems Modeled in SystemC",
booktitle="Verification, Model Checking, and Abstract Interpretation",
year="2024",
publisher="Springer Nature Switzerland",
address="Cham",
pages="187--209",
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.",
isbn="978-3-031-50521-8"
}

{"_id":"divd7o2oZAN6FWEP4","bibbaseid":"tasche-monti-drerup-blohm-herber-huisman-deductiveverificationofparameterizedembeddedsystemsmodeledinsystemc-2024","author_short":["Tasche, P.","Monti, R. E.","Drerup, S. E.","Blohm, P.","Herber, P.","Huisman, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Tasche"],"firstnames":["Philip"],"suffixes":[]},{"propositions":[],"lastnames":["Monti"],"firstnames":["Raúl","E."],"suffixes":[]},{"propositions":[],"lastnames":["Drerup"],"firstnames":["Stefanie","Eva"],"suffixes":[]},{"propositions":[],"lastnames":["Blohm"],"firstnames":["Pauline"],"suffixes":[]},{"propositions":[],"lastnames":["Herber"],"firstnames":["Paula"],"suffixes":[]},{"propositions":[],"lastnames":["Huisman"],"firstnames":["Marieke"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Dimitrova"],"firstnames":["Rayna"],"suffixes":[]},{"propositions":[],"lastnames":["Lahav"],"firstnames":["Ori"],"suffixes":[]},{"propositions":[],"lastnames":["Wolff"],"firstnames":["Sebastian"],"suffixes":[]}],"title":"Deductive Verification of Parameterized Embedded Systems Modeled in SystemC","booktitle":"Verification, Model Checking, and Abstract Interpretation","year":"2024","publisher":"Springer Nature Switzerland","address":"Cham","pages":"187–209","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.","isbn":"978-3-031-50521-8","bibtex":"@InProceedings{Tasche24,\nauthor=\"Tasche, Philip\nand Monti, Ra{\\'u}l E.\nand Drerup, Stefanie Eva\nand Blohm, Pauline\nand Herber, Paula\nand Huisman, Marieke\",\neditor=\"Dimitrova, Rayna\nand Lahav, Ori\nand Wolff, Sebastian\",\ntitle=\"Deductive Verification of Parameterized Embedded Systems Modeled in SystemC\",\nbooktitle=\"Verification, Model Checking, and Abstract Interpretation\",\nyear=\"2024\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"187--209\",\nabstract=\"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.\",\nisbn=\"978-3-031-50521-8\"\n}\n\n","author_short":["Tasche, P.","Monti, R. E.","Drerup, S. E.","Blohm, P.","Herber, P.","Huisman, M."],"editor_short":["Dimitrova, R.","Lahav, O.","Wolff, S."],"key":"Tasche24","id":"Tasche24","bibbaseid":"tasche-monti-drerup-blohm-herber-huisman-deductiveverificationofparameterizedembeddedsystemsmodeledinsystemc-2024","role":"author","urls":{},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":[],"search_terms":["deductive","verification","parameterized","embedded","systems","modeled","systemc","tasche","monti","drerup","blohm","herber","huisman"],"title":"Deductive Verification of Parameterized Embedded Systems Modeled in SystemC","year":2024}