This program is tentative and subject to change.
Complex systems often exhibit multiple behavioural requirements that span different contexts, safety goals, and performance metrics. However, not all requirements share the same level of criticality or compatibility. Some must always be satisfied to ensure safety or correctness, while others may be only desirable under certain conditions. This diversity in importance and compatibility must be carefully considered when designing the system and during its execution. These behavioural requirements are commonly expressed as formal properties. Runtime verification and enforcement frameworks are employed to monitor whether these properties hold over system executions. When violations are detected, enforcement mechanisms must intervene by correcting the system’s executions to bring the execution in line with the specified properties before it is passed on to other components or subsystems. This ensures that the system continues to function within acceptable bounds, even in the presence of deviations or unforeseen behaviours.
Runtime enforcement strategies exhibit a broad design space, capable of handling multiple properties. A common approach is to treat all properties as equally important and enforce them simultaneously. However, depending on the application’s requirements, it may be necessary to adopt alternative enforcement methods that account for the criticality or compatibility of properties. This prevents enforcement conflicts and reduces computational inefficiencies. In this work, we introduce categories of properties based on their enforcement requirements and propose tailored, practical enforcement strategies for each category, thereby improving enforcement efficiency. Thus, when presented with multiple properties, organized in categories, we are able to generate a customized enforcer that respects the context of each category, ensuring that the properties are enforced in a manner aligned with their individual enforcement semantics. We call this framework Context-Aware Runtime Enforcement framework.
This program is tentative and subject to change.
Mon 27 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
11:00 - 12:30 | |||
11:00 30mTalk | Property Grouping and Context-Aware Runtime Enforcement NIER Saumya Shankar International Institute of Information Technology Bangalore, Srinivas Pinisetty Indian Institute of Technology Bhubaneswar, Thierry Jéron INRIA | ||
11:30 30mTalk | Compositional Probabilistic Model Checking with String Diagrams of MDPs NIER Ichiro Hasuo National Institute of Informatics, Japan | ||
12:00 30mTalk | PhantomDrive: A Privacy-Focused Navigation System for Concealing User Movements NIER | ||