Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system

DOI10.1016/J.IPL.2016.02.001MaRDI QIDQ264193zbMATH OpenOpenAlexFDO

Authors Cinzia Bernardeschi, Andrea Domenici

Publication date 6 April 2016

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11568/776232

zbMATH Keywords

verificationnonlinear controlformal methodsprototype verification systemtheorem proving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Nonlinear systems in control theory (93C10) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Recommendations

• scientific article; zbMATH DE number 1746646
• Bellerophon: tactical theorem proving for hybrid systems
• A light-weight integration of automated and interactive theorem proving
• Numerically-aided deductive safety proof for a powertrain control system
• Interactive theorem proving with temporal logic

Cites work

• scientific article; zbMATH DE number 1670737 (Why is no real title available?)
• scientific article; zbMATH DE number 1670744 (Why is no real title available?)
• scientific article; zbMATH DE number 2085344 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
• Hybrid Systems: Computation and Control
• Isabelle/HOL. A proof assistant for higher-order logic
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Modeling and simulation in Scilab/Scicos with ScicosLab 4.4
• Modelling of Complex Systems: Systems as Dataflow Machines
• Simulation of ODE/PDE models with MATLAB, OCTAVE and SCILAB. Scientific and engineering applications
• Untersuchungen über das logische Schliessen. I
• Verified Real Number Calculations: A Library for Interval Arithmetic

Cited in

(6)

• Applications of real number theorem proving in PVS
• A light-weight integration of automated and interactive theorem proving
• Numerically-aided deductive safety proof for a powertrain control system
• Theorem-proving analysis of digital control logic interacting with continuous dynamics
• Bellerophon: tactical theorem proving for hybrid systems
• Verifying a scheduling protocol of safety-critical systems

Describes a project that uses

Uses Software

• Manip
• PVSio-web
• HybridSal
• HSolver
• ScicosLab
• Uppaal
• Benchmarks
• RSOLVER
• NuSMV
• KeYmaera
• PVS
• Scicos
• Isabelle/HOL
• Coq

This page was built for publication: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system

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