Requirements Validation for Hybrid Systems

DOI10.1007/978-3-642-02658-4_17MaRDI QIDQ3636860zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Alessandro Cimatti, Marco Roveri, Stefano Tonetta

Publication date 30 June 2009

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02658-4_17

Mathematics Subject Classification ID

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

• HRELTL: a temporal logic for hybrid systems
• A Temporal Dynamic Logic for Verifying Hybrid System Invariants
• A SOC-based formal specification and verification of hybrid systems
• Hybrid diagrams
• STL model checking of continuous and hybrid systems

Cited in

(9)

• Tightening the contract refinements of a system architecture
• An abstract model for proving safety of autonomous urban traffic
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• Linear-time temporal logic with event freezing functions
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• Quantifier-free encoding of invariants for hybrid systems
• Hierarchical reasoning for the verification of parametric systems
• A refinement-based formal development of cyber-physical railway signalling systems
• HRELTL: a temporal logic for hybrid systems

This page was built for publication: Requirements Validation for Hybrid Systems

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