NDLI: ModelPlex: verified runtime validation of verified cyber-physical system models

Content Provider	Springer Nature Link
Author	Mitsch, Stefan Platzer, André
Copyright Year	2016
Abstract	Formal verification and validation play a crucial role in making cyber-physical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified with respect to the model. Otherwise, all bets are off. This article introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures in a provably correct way that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions, assuming the system dynamics deviation is bounded. This article, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic by a correct-by-construction approach, leading to verifiably correct runtime model validation. Overall, ModelPlex generates provably correct monitor conditions that, if checked to hold at runtime, are provably guaranteed to imply that the offline safety verification results about the CPS model apply to the present run of the actual CPS implementation.
Starting Page	33
Ending Page	74
Page Count	42
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	49
Issue Number	1-2
e-ISSN	15728102
Language	English
Publisher	Springer US
Publisher Date	2016-02-18
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Runtime verification Static verification Cyber-physical systems Hybrid systems Differential dynamic logic Circuits and Systems Electrical Engineering Computer-Aided Engineering (CAD, CAE) and Design Software Engineering/Programming and Operating Systems
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software Hardware and Architecture

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

ModelPlex: verified runtime validation of verified cyber-physical system models

Computing differential invariants of hybrid systems as fixedpoints

Collecting Statistics Over Runtime Executions

Using Static Analysis to Reduce Dynamic Analysis Overhead

Runtime verification with minimal intrusion through parallelism

Time-triggered runtime verification

Runtime enforcement of timed properties revisited

Introduction to the special issue on runtime verification

Runtime verification of embedded real-time systems

ModelPlex: verified runtime validation of verified cyber-physical system models

Similar Documents

ModelPlex: verified runtime validation of verified cyber-physical system models

Computing differential invariants of hybrid systems as fixedpoints

Collecting Statistics Over Runtime Executions

Using Static Analysis to Reduce Dynamic Analysis Overhead

Runtime verification with minimal intrusion through parallelism

Time-triggered runtime verification

Runtime enforcement of timed properties revisited

Introduction to the special issue on runtime verification

Runtime verification of embedded real-time systems

ModelPlex: verified runtime validation of verified cyber-physical system models