Formal Verification of Cyber-Physical Systems Using Domain-Specific Abstractions. Herber, P., Adelt, J., & Tasche, P. In Madeira, A. & Knapp, A., editors, Software Engineering and Formal Methods, pages 3–21, Cham, 2025. Springer Nature Switzerland. abstract bibtex Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring safety and resilience of cyber-physical systems. Formal methods have the potential to guarantee such properties under all circumstances. However, they are expensive and severely suffer from scalability issues. To improve scalability and applicability of formal methods, it is highly desirable to exploit domain-specific knowledge. In this paper, we summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions. In particular, we present our ideas to use domain-specific abstractions to provide 1) reusable semantics encodings that enable us to automatically transform domain-specific system design languages such as SystemC or Simulink into a formal representation, and 2) reusable specification mechanisms for contracts and invariants that can be used for deductive verification of safety and resilience of reactive, hybrid, and learning systems. We discuss promising results and open problems, and identify challenges for future work.
@InProceedings{10.1007/978-3-031-77382-2_1,
author="Herber, Paula
and Adelt, Julius
and Tasche, Philip",
editor="Madeira, Alexandre
and Knapp, Alexander",
title="Formal Verification of Cyber-Physical Systems Using Domain-Specific Abstractions",
booktitle="Software Engineering and Formal Methods",
year="2025",
publisher="Springer Nature Switzerland",
address="Cham",
pages="3--21",
abstract="Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring safety and resilience of cyber-physical systems. Formal methods have the potential to guarantee such properties under all circumstances. However, they are expensive and severely suffer from scalability issues. To improve scalability and applicability of formal methods, it is highly desirable to exploit domain-specific knowledge. In this paper, we summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions. In particular, we present our ideas to use domain-specific abstractions to provide 1) reusable semantics encodings that enable us to automatically transform domain-specific system design languages such as SystemC or Simulink into a formal representation, and 2) reusable specification mechanisms for contracts and invariants that can be used for deductive verification of safety and resilience of reactive, hybrid, and learning systems. We discuss promising results and open problems, and identify challenges for future work.",
isbn="978-3-031-77382-2"
}
Downloads: 0
{"_id":"HW3pC4quzQFsfQyfX","bibbaseid":"herber-adelt-tasche-formalverificationofcyberphysicalsystemsusingdomainspecificabstractions-2025","author_short":["Herber, P.","Adelt, J.","Tasche, P."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Herber"],"firstnames":["Paula"],"suffixes":[]},{"propositions":[],"lastnames":["Adelt"],"firstnames":["Julius"],"suffixes":[]},{"propositions":[],"lastnames":["Tasche"],"firstnames":["Philip"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Madeira"],"firstnames":["Alexandre"],"suffixes":[]},{"propositions":[],"lastnames":["Knapp"],"firstnames":["Alexander"],"suffixes":[]}],"title":"Formal Verification of Cyber-Physical Systems Using Domain-Specific Abstractions","booktitle":"Software Engineering and Formal Methods","year":"2025","publisher":"Springer Nature Switzerland","address":"Cham","pages":"3–21","abstract":"Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring safety and resilience of cyber-physical systems. Formal methods have the potential to guarantee such properties under all circumstances. However, they are expensive and severely suffer from scalability issues. To improve scalability and applicability of formal methods, it is highly desirable to exploit domain-specific knowledge. In this paper, we summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions. In particular, we present our ideas to use domain-specific abstractions to provide 1) reusable semantics encodings that enable us to automatically transform domain-specific system design languages such as SystemC or Simulink into a formal representation, and 2) reusable specification mechanisms for contracts and invariants that can be used for deductive verification of safety and resilience of reactive, hybrid, and learning systems. We discuss promising results and open problems, and identify challenges for future work.","isbn":"978-3-031-77382-2","bibtex":"@InProceedings{10.1007/978-3-031-77382-2_1,\nauthor=\"Herber, Paula\nand Adelt, Julius\nand Tasche, Philip\",\neditor=\"Madeira, Alexandre\nand Knapp, Alexander\",\ntitle=\"Formal Verification of Cyber-Physical Systems Using Domain-Specific Abstractions\",\nbooktitle=\"Software Engineering and Formal Methods\",\nyear=\"2025\",\npublisher=\"Springer Nature Switzerland\",\naddress=\"Cham\",\npages=\"3--21\",\nabstract=\"Cyber-physical systems have become ubiquitous in our daily lives, and their complexity continually evolves to unprecedented levels. In addition to their heterogeneity and interaction with a physical environment, we see a tremendous increase in the use of learning to make autonomous decisions in dynamic environments. These developments pose significant challenges for ensuring safety and resilience of cyber-physical systems. Formal methods have the potential to guarantee such properties under all circumstances. However, they are expensive and severely suffer from scalability issues. To improve scalability and applicability of formal methods, it is highly desirable to exploit domain-specific knowledge. In this paper, we summarize some of our recent efforts towards reusable specification and more scalable verification of cyber-physical systems using domain-specific abstractions. In particular, we present our ideas to use domain-specific abstractions to provide 1) reusable semantics encodings that enable us to automatically transform domain-specific system design languages such as SystemC or Simulink into a formal representation, and 2) reusable specification mechanisms for contracts and invariants that can be used for deductive verification of safety and resilience of reactive, hybrid, and learning systems. We discuss promising results and open problems, and identify challenges for future work.\",\nisbn=\"978-3-031-77382-2\"\n}\n\n","author_short":["Herber, P.","Adelt, J.","Tasche, P."],"editor_short":["Madeira, A.","Knapp, A."],"key":"10.1007/978-3-031-77382-2_1","id":"10.1007/978-3-031-77382-2_1","bibbaseid":"herber-adelt-tasche-formalverificationofcyberphysicalsystemsusingdomainspecificabstractions-2025","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":["formal","verification","cyber","physical","systems","using","domain","specific","abstractions","herber","adelt","tasche"],"title":"Formal Verification of Cyber-Physical Systems Using Domain-Specific Abstractions","year":2025}