Skill-Based Verification of Cyber-Physical Systems

DOI10.1007/978-3-030-45234-6_10OpenAlexW3018387179MaRDI QIDQ5039533

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

Publication date: 13 October 2022

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

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

zbMATH Keywords

hybrid systemstheorem provingautomated reasoningformal methodscyber-physical systemsdeductive verificationdesign by contractKeYmaera X

Mathematics Subject Classification ID

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

Uses Software

• KeYmaera
• JML
• Spec#
• z3

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Differential dynamic logic for hybrid systems
• A theory of timed automata
• A complete uniform substitution calculus for differential dynamic logic
• Hybrid process algebra
• Behavioral interface specification languages
• Logics of Dynamical Systems
• The Complete Proof Theory of Hybrid Systems
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Verification and Control of Hybrid Systems
• Change and Delay Contracts for Hybrid System Component Verification
• Handbook of Hybrid Systems Control

This page was built for publication: Skill-Based Verification of Cyber-Physical Systems