Formal Modelling, Analysis and Verification of Hybrid Systems

DOI10.1007/978-3-642-39721-9_5zbMath1444.68105OpenAlexW35751504MaRDI QIDQ2948232

Naijun Zhan, Heng-Jun Zhao, Shu-Ling Wang

Publication date: 30 September 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39721-9_5

zbMATH Keywords

hybrid systemstheorem provingpolynomial invariantshybrid CSPhybrid Hoare logic

Mathematics Subject Classification ID

Logic in computer science (03B70) 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) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Behavior modeling and verification of movement authority scenario of Chinese Train Control System using AADL ⋮ A compositional modelling and verification framework for stochastic hybrid systems ⋮ A Two-Way Path Between Formal and Informal Design of Embedded Systems ⋮ Barrier certificates revisited ⋮ Manifest domains: analysis and description

Uses Software

• Maple
• QEPCAD
• REDLOG
• RSOLVER
• z3
• HSolver
• Ptolemy
• DISCOVERER
• CESAR
• MathSAT

Cites Work

• Recent advances in program verification through computer algebra
• Controller synthesis for safety and reachability via approximate bisimulation
• The algorithmic analysis of hybrid systems
• Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
• A calculus of durations
• A theory of timed automata
• Duration calculus. A formal approach to real-time systems.
• Recent advances on determining the number of real roots of parametric polynomials
• Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems
• Counterexample-guided predicate abstraction of hybrid systems
• An Assume/Guarantee Based Compositional Calculus for Hybrid CSP
• Deductive Verification of Continuous Dynamical Systems
• Automatic invariant generation for hybrid systems using ideal fixed points
• Measurability and safety verification for stochastic hybrid systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Non-linear loop invariant generation using Gröbner bases
• Computing Differential Invariants of Hybrid Systems as Fixedpoints
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• Synthesizing Switching Logic Using Constraint Solving
• Automatic Synthesis of Robust and Optimal Controllers – An Industrial Case Study
• Multiple Lyapunov functions and other analysis tools for switched and hybrid systems
• A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example
• QEPCAD B
• A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Stability Criteria for Switched and Hybrid Systems
• Theorem Proving in Higher Order Logics
• Automated Technology for Verification and Analysis
• An axiomatic basis for computer programming
• Hybrid Systems: Computation and Control
• Computer Aided Verification
• Symbolic reachability computation for families of linear vector fields
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formal Modelling, Analysis and Verification of Hybrid Systems