Srinivas Pinisetty

Mir Md Sajid Sarwar, Srinivas Pinisetty, Rajarshi Ray et al.

Runtime enforcement has emerged as a promising approach for ensuring the safety of autonomous and cyber-physical systems operating in uncertain and dynamic environments. Unlike traditional runtime verification, runtime enforcement actively intervenes during execution to prevent property violations by modifying unsafe system behaviors. Existing enforcement frameworks primarily focus on untimed or discrete-time specifications and are often limited to delaying or suppressing events, making them inadequate for reactive systems exhibiting complex continuous dynamics. In this paper, we propose a runtime enforcement framework where safety requirements are modeled using Hybrid Automata (HA). The framework combines discrete-event editing with continuous-time monitoring to support enforcement actions such as suppression, delay, and insertion of events at arbitrary time instants. Upon observing environmental inputs, the automaton is initialized, and runtime reachability analysis is used to synthesize safe corrective actions. We formally define the enforcement problem for safety hybrid automata, establish enforceability conditions, and present an online enforcement algorithm for reactive systems. A detailed case study on an Adaptive Cruise Control (ACC) system demonstrates the effectiveness of the proposed approach in maintaining safety properties under unsafe controller behaviors. Experimental results show that the framework introduces minimal computational overhead while ensuring continuous compliance with safety requirements in real time.

Abhinandan Panda, Srinivas Pinisetty, Partha Roop

Biophysical signals such as Electrocardiogram (ECG) and Photoplethysmogram (PPG) are key to the sensing of vital parameters for wellbeing. Coincidentally, ECG and PPG are signals, which provide a "different window" into the same phenomena, namely the cardiac cycle. While they are used separately, there are no studies regarding the exact correction of the different ECG and PPG events. Such correlation would be helpful in many fronts such as sensor fusion for improved accuracy using cheaper sensors and attack detection and mitigation methods using multiple signals to enhance the robustness, for example. Considering this, we present the first approach in formally establishing the key relationships between ECG and PPG signals. We combine formal run-time monitoring with statistical analysis and regression analysis for our results.

Hammond Pearce, Xin Yang, Srinivas Pinisetty et al.

Cyber-Physical Systems (CPSs) such as those found within autonomous vehicles are increasingly adopting Artificial Neural Network (ANN)-based controllers. To ensure the safety of these controllers, there is a spate of recent activity to formally verify the ANN-based designs. There are two challenges with these approaches: (1) The verification of such systems is difficult and time consuming. (2) These verified controllers are not able to adapt to frequent requirements changes, which are typical in situations like autonomous driving. This raises the question: how can trained and verified controllers, which have gone through expensive training and verification processes, be re-used to deal with requirement changes? This paper addresses this challenge for the first time by proposing a new framework that is capable of dealing with requirement changes at runtime through a mechanism we term runtime interchange. Our approach functions via a continual exchange and selection process of multiple pre-verified controllers. It represents a key step on the way to component-oriented engineering for intelligent designs, as it preserves the behaviours of the original controllers while introducing additional functionality. To demonstrate the efficacy of our approach we utilise an existing autonomous driving case study as well as a set of smaller benchmarks. These show that introduced overheads are extremely minimal and that the approach is very scalable.

Srinivas Pinisetty, Thibaud Antignac, David Sands et al.

Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking that a program satisfies the data minimisation principle is not easy, even for the simple case when considering deterministic programs-as-functions. In this paper we prove (im)possibility results concerning runtime monitoring of (non-)minimality for deterministic programs both when the program has one input source (monolithic) and for the more general case when inputs come from independent sources (distributed case). We propose monitoring mechanisms where a monitor observes the inputs and the outputs of a program, to detect violation of data minimisation policies. We show that monitorability of (non) minimality is decidable only for specific cases, and detection of satisfaction of different notions of minimality in undecidable in general. That said, we show that under certain conditions monitorability is decidable and we provide an algorithm and a bound to check such properties in a pre-deployment controlled environment, also being able to compute a minimiser for the given program. Finally, we provide a proof-of-concept implementation for both offline and online monitoring and apply that to some case studies.

Srinivas Pinisetty, Partha S Roop, Steven Smyth et al.

Synchronous programming is a paradigm of choice for the design of safety-critical reactive systems. Runtime enforcement is a technique to ensure that the output of a black-box system satisfies some desired properties. This paper deals with the problem of runtime enforcement in the context of synchronous programs. We propose a framework where an enforcer monitors both the inputs and the outputs of a synchronous program and (minimally) edits erroneous inputs/outputs in order to guarantee that a given property holds. We define enforceability conditions, develop an online enforcement algorithm, and prove its correctness. We also report on an implementation of the algorithm on top of the KIELER framework for the SCCharts synchronous language. Experimental results show that enforcement has minimal execution time overhead, which decreases proportionally with larger benchmarks.