NDLI: Forward invariant cuts to simplify proofs of safety

Content Provider	IEEE Xplore Digital Library
Author	Aréchiga, N. Kapinski, J. Deshmukh, J.V. Platzer, A. Krogh, B.
Copyright Year	2015
Abstract	The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems; however, state-of-the-art theorem provers require manual intervention to handle complex systems. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assistance that a system designer is able to provide directly. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about performance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage forward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing automatic verification approaches using several examples, including one involving an automotive powertrain control system.
Starting Page	227
Ending Page	236
File Size	856475
Page Count	10
File Format	PDF
ISBN	9781467380799
DOI	10.1109/EMSOFT.2015.7318278
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2015-10-04
Publisher Place	Netherlands
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Semantics Automata Theorem provers Hybrid systems Cognition Safety Mathematical model Lyapunov methods Automotive engineering Formal verification
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Forward invariant cuts to simplify proofs of safety

Formal verification of hybrid systems

Forward Invariant Cuts to Simplify Proofs of Safety

Safety Verification of Non-linear, Planar Proportional Control with Differential Inclusions

Time-aware relational abstractions for hybrid systems

Formal verification of control systems' properties with theorem proving

AADL Execution Semantics Transformation for Formal Verification

Stability of hybrid automata with average dwell time: an invariant approach

Formal verification of hybrid systems using CheckMate: a case study

Forward invariant cuts to simplify proofs of safety

Similar Documents

Forward invariant cuts to simplify proofs of safety

Formal verification of hybrid systems

Forward Invariant Cuts to Simplify Proofs of Safety

Safety Verification of Non-linear, Planar Proportional Control with Differential Inclusions

Time-aware relational abstractions for hybrid systems

Formal verification of control systems' properties with theorem proving

AADL Execution Semantics Transformation for Formal Verification

Stability of hybrid automata with average dwell time: an invariant approach

Formal verification of hybrid systems using CheckMate: a case study

Forward invariant cuts to simplify proofs of safety