Skill-based verification of cyber-physical systems

DOI10.1007/978-3-030-45234-6_10MaRDI QIDQ5039533zbMATH OpenOpenAlexFDO

Authors Alexander Knüppel, Inga Jatzkowski, Marcus Nolte, Thomas Thüm, Tobias Runge, Ina Schaefer

Publication date 13 October 2022

Published in Fundamental Approaches to Software Engineering (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-45234-6_10

zbMATH Keywords

hybrid systemsformal methodstheorem provingautomated reasoningcyber-physical systemsdeductive verificationdesign by contractKeYmaera X

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Recommendations

• scientific article; zbMATH DE number 6719346
• \textsc{DryVR}: data-driven verification and compositional reasoning for automotive systems
• On minimising the maximum expected verification time
• Heterogeneous verification of cyber-physical systems using behavior relations
• Verifying autonomous systems

Cites work

• scientific article; zbMATH DE number 6020480 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• scientific article; zbMATH DE number 7361375 (Why is no real title available?)
• A complete uniform substitution calculus for differential dynamic logic
• A theory of timed automata
• Behavioral interface specification languages
• Change and delay contracts for hybrid system component verification
• Differential dynamic logic for hybrid systems
• Handbook of Hybrid Systems Control
• Hybrid process algebra
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Logics of dynamical systems
• The Complete Proof Theory of Hybrid Systems
• Verification and Control of Hybrid Systems

Describes a project that uses

Uses Software

• z3
• Spec#
• JML
• KeYmaera

This page was built for publication: Skill-based verification of cyber-physical systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5039533)