Compositional runtime enforcement

Srinivas Pinisetty, Stavros Tripakis

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)

Abstract

Runtime enforcement is a methodology used to enforce that the output of a running system satisfies a desired property. Given a property, an enforcement monitor modifies an (untrusted) sequence of events into a sequence that complies to that property. In practice, we may have not one, but many properties to enforce. Moreover, new properties may arise as new capabilities are added to the system. It then becomes interesting to be able to build not a single, monolithic monitor that enforces all the properties, but rather several monitors, one for each property. The question is to what extent such monitors can be composed, and how. This is the topic of this paper. We study two monitor composition schemes, serial and parallel composition, and show that, while enforcement under these schemes is generally not compositional, it is for certain subclasses of regular properties.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7-9, 2016, Proceedings
EditorsSanjai Rayadurgam , Oksana Tkachuk
PublisherSpringer International Publishing
Pages82-99
Volume9690
ISBN (Electronic)978-3-319-40648-0
ISBN (Print)978-3-319-40647-3
DOIs
Publication statusPublished - 2016
MoE publication typeA4 Article in a conference publication
EventInternational Symposium on NASA Formal Methods - Minneapolis, United States
Duration: 7 Jun 20169 Jun 2016
Conference number: 8

Publication series

NameLecture Notes in Computer Science
Volume9690
ISSN (Print)0302-9743

Conference

ConferenceInternational Symposium on NASA Formal Methods
Abbreviated titleNFM
Country/TerritoryUnited States
CityMinneapolis
Period07/06/201609/06/2016

Fingerprint

Dive into the research topics of 'Compositional runtime enforcement'. Together they form a unique fingerprint.

Cite this