NDLI: Runtime enforcement of timed properties revisited

Content Provider	Springer Nature Link
Author	Pinisetty, Srinivas Falcone, Yliès Jéron, Thierry Marchand, Hervé Rollet, Antoine Nguena Timo, Omer
Copyright Year	2014
Abstract	Runtime enforcement is a powerful technique to ensure that a running system satisfies some desired properties. Using an enforcement monitor, an (untrustworthy) input execution (in the form of a sequence of events) is modified into an output sequence that complies with a property. Over the last decade, runtime enforcement has been mainly studied in the context of untimed properties. This paper deals with runtime enforcement of timed properties by revisiting the foundations of runtime enforcement when time between events matters. We propose a new enforcement paradigm where enforcement mechanisms are time retardants: to produce a correct output sequence, additional delays are introduced between the events of the input sequence. We consider runtime enforcement of any regular timed property defined by a timed automaton. We prove the correctness of enforcement mechanisms and prove that they enjoy two usually expected features, revisited here in the context of timed properties. The first one is soundness meaning that the output sequences (eventually) satisfy the required property. The second one is transparency, meaning that input sequences are modified in a minimal way. We also introduce two new features, (i) physical constraints that describe how a time retardant is physically constrained when delaying a sequence of timed events, and (ii) optimality, meaning that output sequences are produced as soon as possible. To facilitate the adoption and implementation of enforcement mechanisms, we describe them at several complementary abstraction levels. Our enforcement mechanisms have been implemented and our experimental results demonstrate the feasibility of runtime enforcement in a timed context and the effectiveness of the mechanisms.
Starting Page	381
Ending Page	422
Page Count	42
File Format	PDF
ISSN	09259856
Journal	Formal Methods in System Design
Volume Number	45
Issue Number	3
e-ISSN	15728102
Language	English
Publisher	Springer US
Publisher Date	2014-10-28
Publisher Place	Boston
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Runtime verification Runtime enforcement Timed properties Timed automata Software engineering 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

Verification of continuous dynamical systems by timed automata

Interrupt Timed Automata: verification and expressiveness

Timed verification of the generic architecture of a memory circuit using parametric timed automata

Checking Timed Büchi Automata Emptiness Efficiently

Decision problems for lower/upper bound parametric timed automata

A game approach to determinize timed automata

MSO logics for weighted timed automata

Model checking for probabilistic timed automata

Introduction to the special issue on runtime verification

Runtime enforcement of timed properties revisited

Similar Documents

Verification of continuous dynamical systems by timed automata

Interrupt Timed Automata: verification and expressiveness

Timed verification of the generic architecture of a memory circuit using parametric timed automata

Checking Timed Büchi Automata Emptiness Efficiently

Decision problems for lower/upper bound parametric timed automata

A game approach to determinize timed automata

MSO logics for weighted timed automata

Model checking for probabilistic timed automata

Introduction to the special issue on runtime verification

Runtime enforcement of timed properties revisited