research-article

Runtime enforcement of regular timed properties

Authors:

Srinivas Pinisetty,

Yliès Falcone,

Thierry Jéron,

Hervé MarchandAuthors Info & Claims

SAC '14: Proceedings of the 29th Annual ACM Symposium on Applied Computing

Pages 1279 - 1286

https://doi.org/10.1145/2554850.2554967

Published: 24 March 2014 Publication History

Get Access

Abstract

Runtime enforcement is a verification/validation technique aiming at correcting (possibly incorrect) executions of a system of interest. In this paper, we consider enforcement monitoring for systems with timed specifications (modeled as timed automata). We consider runtime enforcement of any regular timed property specified by a timed automaton. To ease their design and their correctness-proof, enforcement mechanisms are described at several levels: enforcement functions that specify the input-output behavior, constraints that should be satisfied by such functions, enforcement monitors that implement an enforcement function as a transition system, and enforcement algorithms that describe the implementation of enforcement monitors. The feasibility of enforcement monitoring for timed properties is validated by prototyping the synthesis of enforcement monitors.

References

[1]

R. Alur and D. L. Dill. A theory of timed automata. Theoretical Comp. Science, 126: 183--235, 1994.

Digital Library

Google Scholar

[2]

N. Bielova and F. Massacci. Do you really mean what you actually enforced? - edited automata revisited. Int. J. Inf. Sec., 10(4): 239--254, 2011.

Digital Library

Google Scholar

[3]

Y. Falcone. You should better enforce than verify. In Runtime Verification, LNCS, pages 89--105, 2010.

Digital Library

Google Scholar

[4]

Y. Falcone, J.-C. Fernandez, and L. Mounier. What can you verify and enforce at runtime? STTT, 14(3): 349--382, 2012.

Digital Library

Google Scholar

[5]

Y. Falcone, L. Mounier, J.-C. Fernandez, and J.-L. Richier. Runtime enforcement monitors: composition, synthesis, and enforcement abilities. FMSD, 38(3): 223--262, 2011.

Digital Library

Google Scholar

[6]

K. W. Hamlen, G. Morrisett, and F. B. Schneider. Computability classes for enforcement mechanisms. ACM Trans. Program. Lang. Syst., 28(1): 175--205, 2006.

Digital Library

Google Scholar

[7]

J. Ligatti, L. Bauer, and D. Walker. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur., 12(3): 19:1--19:41, 2009.

Digital Library

Google Scholar

[8]

I. Matteucci. Automated synthesis of enforcing mechanisms for security properties in a timed setting. Electr. Notes Theor. Comput. Sci., 186: 101--120, 2007.

Digital Library

Google Scholar

[9]

S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet, and O. L. N. Timo. Runtime enforcement of timed properties. In Runtime Verification, LNCS, 2012.

Google Scholar

[10]

F. B. Schneider. Enforceable security policies. ACM Trans. Inf. Syst. Secur., 3(1): 30--50, 2000.

Digital Library

Google Scholar

[11]

M. Viswanathan and M. Kim. Foundations for the run-time monitoring of reactive systems - Fundamentals of the MaC language. In ICTAC, LNCS, pages 543--556, 2004.

Digital Library

Google Scholar

Cited By

View all

Aceto LCassar IFrancalanza AIngólfsdóttir A(2023)On first-order runtime enforcement of branching-time propertiesActa Informatica10.1007/s00236-023-00441-960:4(385-451)Online publication date: 3-Aug-2023
https://doi.org/10.1007/s00236-023-00441-9
Gupta GShankar SPinisetty S(2022)Automated Surgical Procedure Assistance Framework Using Deep Learning and Formal Runtime MonitoringRuntime Verification10.1007/978-3-031-17196-3_2(25-44)Online publication date: 23-Sep-2022
https://doi.org/10.1007/978-3-031-17196-3_2
Pinisetty SAllen NPearce HTrew MSingh Gaur MRoop P(2022) Formal Methods for the Security of Medical Devices 1 Applied Smart Health Care Informatics10.1002/9781119743187.ch3(31-65)Online publication date: 25-Feb-2022
https://doi.org/10.1002/9781119743187.ch3
Show More Cited By

Index Terms

Runtime enforcement of regular timed properties

Recommendations

Serial Compositional Runtime Enforcement of Safety Timed Properties
ISEC '23: Proceedings of the 16th Innovations in Software Engineering Conference

Runtime enforcement is a mechanism that compels a (black-box) system to obey some expected properties. For that, it employs an enforcement monitor /enforcer which modifies an (untrusted) sequence of events into a sequence that complies with the ...
Runtime enforcement of regular timed properties by suppressing and delaying events

Runtime enforcement is a verification/validation technique aiming at correcting possibly incorrect executions of a system of interest. In this paper, we consider enforcement monitoring for systems where the physical time elapsing between actions ...
Runtime enforcement of timed properties revisited

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 ...

Comments

Information & Contributors

Information

Published In

SAC '14: Proceedings of the 29th Annual ACM Symposium on Applied Computing

March 2014

1890 pages

ISBN:9781450324694

DOI:10.1145/2554850

Conference Chairs:
Yookun Cho
Seoul National University, Korea
,
Sung Y. Shin
South Dakota State University
,
Program Chairs:
Sangwook Kim
Kyungpook National University, Korea
,
Chih-Cheng Hung
Southern Polytechnic State University
,
Jiman Hong
Soongsil University, South Korea

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 March 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

SAC 2014

Sponsor:

SIGAPP

SAC 2014: Symposium on Applied Computing

March 24 - 28, 2014

Gyeongju, Republic of Korea

Acceptance Rates

SAC '14 Paper Acceptance Rate 218 of 939 submissions, 23%;

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
76
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Aceto LCassar IFrancalanza AIngólfsdóttir A(2023)On first-order runtime enforcement of branching-time propertiesActa Informatica10.1007/s00236-023-00441-960:4(385-451)Online publication date: 3-Aug-2023
https://doi.org/10.1007/s00236-023-00441-9
Gupta GShankar SPinisetty S(2022)Automated Surgical Procedure Assistance Framework Using Deep Learning and Formal Runtime MonitoringRuntime Verification10.1007/978-3-031-17196-3_2(25-44)Online publication date: 23-Sep-2022
https://doi.org/10.1007/978-3-031-17196-3_2
Pinisetty SAllen NPearce HTrew MSingh Gaur MRoop P(2022) Formal Methods for the Security of Medical Devices 1 Applied Smart Health Care Informatics10.1002/9781119743187.ch3(31-65)Online publication date: 25-Feb-2022
https://doi.org/10.1002/9781119743187.ch3
Renard MRollet AFalcone Y(2020)Runtime enforcement of timed properties using gamesFormal Aspects of Computing10.1007/s00165-020-00515-2Online publication date: 28-Jul-2020
https://doi.org/10.1007/s00165-020-00515-2
Massoud RLe HChini PSaivasan PMeyer RDrechsler R(2019)Temporal Tracing of On-Chip Signals using TimeprintsProceedings of the 56th Annual Design Automation Conference 201910.1145/3316781.3317920(1-6)Online publication date: 2-Jun-2019
https://dl.acm.org/doi/10.1145/3316781.3317920
Falcone YPinisetty S(2019)On the Runtime Enforcement of Timed PropertiesRuntime Verification10.1007/978-3-030-32079-9_4(48-69)Online publication date: 1-Oct-2019
https://doi.org/10.1007/978-3-030-32079-9_4
Falcone YMariani LRollet ASaha S(2018)Runtime Failure Prevention and ReactionLectures on Runtime Verification10.1007/978-3-319-75632-5_4(103-134)Online publication date: 11-Feb-2018
https://doi.org/10.1007/978-3-319-75632-5_4
Pinisetty SPreoteasa VTripakis SJéron TFalcone YMarchand H(2017)Predictive runtime enforcementFormal Methods in System Design10.1007/s10703-017-0271-151:1(154-199)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10703-017-0271-1
Renard MFalcone YRollet APinisetty SJéron TMarchand H(2015)Enforcement of Timed Properties with Uncontrollable EventsProceedings of the 12th International Colloquium on Theoretical Aspects of Computing - ICTAC 2015 - Volume 939910.1007/978-3-319-25150-9_31(542-560)Online publication date: 29-Oct-2015
https://dl.acm.org/doi/10.1007/978-3-319-25150-9_31
Pinisetty SFalcone YJéron TMarchand HRollet ANguena Timo O(2014)Runtime enforcement of timed properties revisitedFormal Methods in System Design10.1007/s10703-014-0215-y45:3(381-422)Online publication date: 1-Dec-2014
https://dl.acm.org/doi/10.1007/s10703-014-0215-y

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Index Terms

Recommendations

Serial Compositional Runtime Enforcement of Safety Timed Properties