Proving the Correctness of the Implementation of a Control-Command Algorithm

DOI10.1007/978-3-642-03237-0_9MaRDI QIDQ3392923zbMATH OpenOpenAlexFDO

Authors Olivier Bouissou

Publication date 18 August 2009

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03237-0_9

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The algorithmic analysis of hybrid systems
• Theorem-proving analysis of digital control logic interacting with continuous dynamics
• Closed loop analysis of control command software
• scientific article; zbMATH DE number 1303060
• Periodically Controlled Hybrid Systems

Cites work

• A Hybrid Denotational Semantics for Hybrid Systems
• Abstract Interpretation Frameworks
• Abstract Interpretation of the Physical Inputs of Embedded Programs
• scientific article; zbMATH DE number 1301619 (Why is no real title available?)
• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• scientific article; zbMATH DE number 2080778 (Why is no real title available?)
• scientific article; zbMATH DE number 1507210 (Why is no real title available?)
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Numerical Software with Result Verification
• Periodically Controlled Hybrid Systems
• Proving non-termination
• Proving that programs eventually do something good
• Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization
• Static Analysis in Disjunctive Numerical Domains
• Static Analysis of Numerical Algorithms
• Switching in systems and control
• Uniform Stability of Switched Linear Systems: Extensions of LaSalle's Invariance Principle
• Validated solutions of initial value problems for ordinary differential equations
• Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis

Cited in

(5)

• Theorem-proving analysis of digital control logic interacting with continuous dynamics
• Proof of Correctness of Decision Table Programs
• A proof of protocol correctness
• scientific article; zbMATH DE number 1487482 (Why is no real title available?)
• Proving the correctness of behavioural implementations

Describes a project that uses

Uses Software

• GRKLib
• PHAVer
• ASTREE
• HyTech

This page was built for publication: Proving the Correctness of the Implementation of a Control-Command Algorithm

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