-
The Future of Software Engineering in an AI-Driven World
Authors:
Valerio Terragni,
Partha Roop,
Kelly Blincoe
Abstract:
A paradigm shift is underway in Software Engineering, with AI systems such as LLMs gaining increasing importance for improving software development productivity. This trend is anticipated to persist. In the next five years, we will likely see an increasing symbiotic partnership between human developers and AI. The Software Engineering research community cannot afford to overlook this trend; we mus…
▽ More
A paradigm shift is underway in Software Engineering, with AI systems such as LLMs gaining increasing importance for improving software development productivity. This trend is anticipated to persist. In the next five years, we will likely see an increasing symbiotic partnership between human developers and AI. The Software Engineering research community cannot afford to overlook this trend; we must address the key research challenges posed by the integration of AI into the software development process. In this paper, we present our vision of the future of software development in an AI-Driven world and explore the key challenges that our research community should address to realize this vision.
△ Less
Submitted 11 June, 2024;
originally announced June 2024.
-
Logical Synchrony Networks: A formal model for deterministic distribution
Authors:
Logan Kenwright,
Partha Roop,
Nathan Allen,
Sanjay Lall,
Calin Cascaval,
Tammo Spalink,
Martin Izzard
Abstract:
Kahn Process Networks (KPNs) are a deterministic Model of Computation (MoC) for distributed systems. KPNs supports non-blocking writes and blocking reads, with the consequent assumption of unbounded buffers between processes. Variants such as Finite FIFO Platforms (FFP) have been developed, which enforce boundedness. One issue with existing models is that they mix process synchronisation with proc…
▽ More
Kahn Process Networks (KPNs) are a deterministic Model of Computation (MoC) for distributed systems. KPNs supports non-blocking writes and blocking reads, with the consequent assumption of unbounded buffers between processes. Variants such as Finite FIFO Platforms (FFP) have been developed, which enforce boundedness. One issue with existing models is that they mix process synchronisation with process execution. In this paper we address how these two facets may be decoupled.
This paper explores a recent alternative called bittide, which decouples the execution of a process from the control needed for process synchronisation, and thus preserves determinism and boundedness while ensuring pipelined execution for better throughput. Our intuition is that such an approach could leverage not only determinism and buffer boundedness but may potentially offer better overall throughput.
To understand the behavior of these systems we define a formal model -- a deterministic MoC called Logical Synchrony Networks (LSNs). LSNs describes a network of processes modelled as a graph, with edges representing invariant logical delays between a producer process and the corresponding consumer process. We show that this abstraction is satisfied by KPNs. Subsequently, we show that both FFPs and bittide faithfully implement this abstraction. Thus, we show for the first time that FFPs and bittide offer two alternative ways of implementing deterministic distributed systems with the latter being more performant.
△ Less
Submitted 5 June, 2024; v1 submitted 12 February, 2024;
originally announced February 2024.
-
S-T CRF: Spatial-Temporal Conditional Random Field for Human Trajectory Prediction
Authors:
Pengqian Han,
Jiamou Liu,
Jialing He,
Zeyu Zhang,
Song Yang,
Yanni Tang,
Partha Roop
Abstract:
Trajectory prediction is of significant importance in computer vision. Accurate pedestrian trajectory prediction benefits autonomous vehicles and robots in planning their motion. Pedestrians' trajectories are greatly influenced by their intentions. Prior studies having introduced various deep learning methods only pay attention to the spatial and temporal information of trajectory, overlooking the…
▽ More
Trajectory prediction is of significant importance in computer vision. Accurate pedestrian trajectory prediction benefits autonomous vehicles and robots in planning their motion. Pedestrians' trajectories are greatly influenced by their intentions. Prior studies having introduced various deep learning methods only pay attention to the spatial and temporal information of trajectory, overlooking the explicit intention information. In this study, we introduce a novel model, termed the \textbf{S-T CRF}: \textbf{S}patial-\textbf{T}emporal \textbf{C}onditional \textbf{R}andom \textbf{F}ield, which judiciously incorporates intention information besides spatial and temporal information of trajectory. This model uses a Conditional Random Field (CRF) to generate a representation of future intentions, greatly improving the prediction of subsequent trajectories when combined with spatial-temporal representation. Furthermore, the study innovatively devises a space CRF loss and a time CRF loss, meticulously designed to enhance interaction constraints and temporal dynamics, respectively. Extensive experimental evaluations on dataset ETH/UCY and SDD demonstrate that the proposed method surpasses existing baseline approaches.
△ Less
Submitted 29 November, 2023;
originally announced November 2023.
-
STF: Spatial Temporal Fusion for Trajectory Prediction
Authors:
Pengqian Han,
Partha Roop,
Jiamou Liu,
Tianzhe Bao,
Yifei Wang
Abstract:
Trajectory prediction is a challenging task that aims to predict the future trajectory of vehicles or pedestrians over a short time horizon based on their historical positions. The main reason is that the trajectory is a kind of complex data, including spatial and temporal information, which is crucial for accurate prediction. Intuitively, the more information the model can capture, the more preci…
▽ More
Trajectory prediction is a challenging task that aims to predict the future trajectory of vehicles or pedestrians over a short time horizon based on their historical positions. The main reason is that the trajectory is a kind of complex data, including spatial and temporal information, which is crucial for accurate prediction. Intuitively, the more information the model can capture, the more precise the future trajectory can be predicted. However, previous works based on deep learning methods processed spatial and temporal information separately, leading to inadequate spatial information capture, which means they failed to capture the complete spatial information. Therefore, it is of significance to capture information more fully and effectively on vehicle interactions. In this study, we introduced an integrated 3D graph that incorporates both spatial and temporal edges. Based on this, we proposed the integrated 3D graph, which considers the cross-time interaction information. In specific, we design a Spatial-Temporal Fusion (STF) model including Multi-layer perceptions (MLP) and Graph Attention (GAT) to capture the spatial and temporal information historical trajectories simultaneously on the 3D graph. Our experiment on the ApolloScape Trajectory Datasets shows that the proposed STF outperforms several baseline methods, especially on the long-time-horizon trajectory prediction.
△ Less
Submitted 29 November, 2023;
originally announced November 2023.
-
Runtime Monitoring and Statistical Approaches for Correlation Analysis of ECG and PPG
Authors:
Abhinandan Panda,
Srinivas Pinisetty,
Partha Roop
Abstract:
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 correlat…
▽ More
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.
△ Less
Submitted 20 January, 2022;
originally announced February 2022.
-
Runtime Interchange for Adaptive Re-use of Intelligent Cyber-Physical System Controllers
Authors:
Hammond Pearce,
Xin Yang,
Srinivas Pinisetty,
Partha S. Roop
Abstract:
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) The…
▽ More
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.
△ Less
Submitted 23 September, 2021;
originally announced October 2021.
-
Designing Neural Networks for Real-Time Systems
Authors:
Hammond Pearce,
Xin Yang,
Partha S. Roop,
Marc Katzef,
Tórur Biskopstø Strøm
Abstract:
Artificial Neural Networks (ANNs) are increasingly being used within safety-critical Cyber-Physical Systems (CPSs). They are often co-located with traditional embedded software, and may perform advisory or control-based roles. It is important to validate both the timing and functional correctness of these systems. However, most approaches in the literature consider guaranteeing only the functional…
▽ More
Artificial Neural Networks (ANNs) are increasingly being used within safety-critical Cyber-Physical Systems (CPSs). They are often co-located with traditional embedded software, and may perform advisory or control-based roles. It is important to validate both the timing and functional correctness of these systems. However, most approaches in the literature consider guaranteeing only the functionality of ANN based controllers. This issue stems largely from the implementation strategies used within common neural network frameworks -- their underlying source code is often simply unsuitable for formal techniques such as static timing analysis. As a result, developers of safety-critical CPS must rely on informal techniques such as measurement based approaches to prove correctness, techniques that provide weak guarantees at best. In this work we address this challenge. We propose a design pipeline whereby neural networks trained using the popular deep learning framework Keras are compiled to functionally equivalent C code. This C code is restricted to simple constructs that may be analysed by existing static timing analysis tools. As a result, if compiled to a suitable time-predictable platform all execution bounds may be statically derived. To demonstrate the benefits of our approach we execute an ANN trained to drive an autonomous vehicle around a race track. We compile the ANN to the Patmos time-predictable controller, and show that we can derive worst case execution timings.
△ Less
Submitted 26 August, 2020;
originally announced August 2020.
-
Quantized State Hybrid Automata for Cyber-Physical Systems
Authors:
Avinash Malik,
Partha Roop
Abstract:
Cyber-physical systems involve a network of discrete controllers that control physical processes. Examples range from autonomous cars to implantable medical devices, which are highly safety critical. Hybrid Automata (HA) based formal approach is gaining momentum for the specification and validation of CPS. HA combines the model of the plant along with its discrete controller resulting in a piece-w…
▽ More
Cyber-physical systems involve a network of discrete controllers that control physical processes. Examples range from autonomous cars to implantable medical devices, which are highly safety critical. Hybrid Automata (HA) based formal approach is gaining momentum for the specification and validation of CPS. HA combines the model of the plant along with its discrete controller resulting in a piece-wise continuous system with discontinuities. Accurate detection of these discontinuities, using appropriate level crossing detectors, is a key challenge to simulation of CPS based on HA. Existing techniques employ time discrete numerical integration with bracketing for level crossing detection. These techniques involve back-tracking and are highly non-deterministic and hence error prone. As level crossings happen based on the values of continuous variables, Quantized State System (QSS)- integration may be more suitable. Existing QSS integrators, based on fixed quanta, are also unsuitable for simulating HAs. This is since the quantum selected is not dependent on the HA guard conditions, which are the main cause of discontinuities. Considering this, we propose a new dynamic quanta based formal model called Quantized State Hybrid Automata (QSHA). The developed formal model and the associated simulation framework guarantees that (1) all level crossings are accurately detected and (2) the time of the level crossing is also accurate within floating point error bounds. Interestingly, benchmarking results reveal that the proposed simulation technique takes 720, 1.33 and 4.41 times fewer simulation steps compared to standard Quantized State System (QSS)-1, Runge-Kutta (RK)-45, and Differential Algebraic System Solver (DASSL) integration based techniques respectively.
△ Less
Submitted 14 June, 2018;
originally announced June 2018.
-
An intracardiac electrogram model to bridge virtual hearts and implantable cardiac devices
Authors:
Weiwei Ai,
Nitish Patel,
Partha Roop,
Avinash Malik,
Nathan Allen,
Mark L. Trew
Abstract:
Virtual heart models have been proposed to enhance the safety of implantable cardiac devices through closed loop validation. To communicate with a virtual heart, devices have been driven by cardiac signals at specific sites. As a result, only the action potentials of these sites are sensed. However, the real device implanted in the heart will sense a complex combination of near and far-field extra…
▽ More
Virtual heart models have been proposed to enhance the safety of implantable cardiac devices through closed loop validation. To communicate with a virtual heart, devices have been driven by cardiac signals at specific sites. As a result, only the action potentials of these sites are sensed. However, the real device implanted in the heart will sense a complex combination of near and far-field extracellular potential signals. Therefore many device functions, such as blanking periods and refractory periods, are designed to handle these unexpected signals. To represent these signals, we develop an intracardiac electrogram (IEGM) model as an interface between the virtual heart and the device. The model can capture not only the local excitation but also far-field signals and pacing afterpotentials. Moreover, the sensing controller can specify unipolar or bipolar electrogram (EGM) sensing configurations and introduce various oversensing and undersensing modes. The simulation results show that the model is able to reproduce clinically observed sensing problems, which significantly extends the capabilities of the virtual heart model in the context of device validation.
△ Less
Submitted 3 March, 2017;
originally announced March 2017.
-
Runtime enforcement of reactive systems using synchronous enforcers
Authors:
Srinivas Pinisetty,
Partha S Roop,
Steven Smyth,
Stavros Tripakis,
Reinhard von Hanxleden
Abstract:
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…
▽ More
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.
△ Less
Submitted 15 December, 2016;
originally announced December 2016.
-
Regularity of the Solution to 1-D Fractional Order Diffusion Equations
Authors:
V. J. Ervin,
N. Heuer,
J. P. Roop
Abstract:
In this article we investigate the solution of the steady-state fractional diffusion equation on a bounded domain in $\real^{1}$. From an analysis of the underlying model problem, we postulate that the fractional diffusion operator in the modeling equations is neither the Riemann-Liouville nor the Caputo fractional differential operators. We then find a closed form expression for the kernel of the…
▽ More
In this article we investigate the solution of the steady-state fractional diffusion equation on a bounded domain in $\real^{1}$. From an analysis of the underlying model problem, we postulate that the fractional diffusion operator in the modeling equations is neither the Riemann-Liouville nor the Caputo fractional differential operators. We then find a closed form expression for the kernel of the fractional diffusion operator which, in most cases, determines the regularity of the solution. Next we establish that the Jacobi polynomials are pseudo eigenfunctions for the fractional diffusion operator. A spectral type approximation method for the solution of the steady-state fractional diffusion equation is then proposed and studied.
△ Less
Submitted 30 July, 2016;
originally announced August 2016.
-
Towards the Emulation of the Cardiac Conduction System for Pacemaker Testing
Authors:
Eugene Yip,
Sidharta Andalam,
Partha S. Roop,
Avinash Malik,
Mark Trew,
Weiwei Ai,
Nitish Patel
Abstract:
The heart is a vital organ that relies on the orchestrated propagation of electrical stimuli to coordinate each heart beat. Abnormalities in the heart's electrical behaviour can be managed with a cardiac pacemaker. Recently, the closed-loop testing of pacemakers with an emulation (real-time simulation) of the heart has been proposed. An emulated heart would provide realistic reactions to the pacem…
▽ More
The heart is a vital organ that relies on the orchestrated propagation of electrical stimuli to coordinate each heart beat. Abnormalities in the heart's electrical behaviour can be managed with a cardiac pacemaker. Recently, the closed-loop testing of pacemakers with an emulation (real-time simulation) of the heart has been proposed. An emulated heart would provide realistic reactions to the pacemaker as if it were a real heart. This enables developers to interrogate their pacemaker design without having to engage in costly or lengthy clinical trials. Many high-fidelity heart models have been developed, but are too computationally intensive to be simulated in real-time. Heart models, designed specifically for the closed-loop testing of pacemakers, are too abstract to be useful in the testing of physical pacemakers.
In the context of pacemaker testing, this paper presents a more computationally efficient heart model that generates realistic continuous-time electrical signals. The heart model is composed of cardiac cells that are connected by paths. Significant improvements were made to an existing cardiac cell model to stabilise its activation behaviour and to an existing path model to capture the behaviour of continuous electrical propagation. We provide simulation results that show our ability to faithfully model complex re-entrant circuits (that cause arrhythmia) that existing heart models can not.
△ Less
Submitted 17 March, 2016; v1 submitted 16 March, 2016;
originally announced March 2016.
-
A synchronous rendering of hybrid systems for designing Plant-on-a-Chip (PoC)
Authors:
Avinash Malik,
Partha S Roop,
Sidharta Andalam,
Eugene Yip,
Mark Trew
Abstract:
Hybrid systems are discrete controllers that are used for controlling a physical process (plant) exhibiting continuous dynamics. A hybrid automata (HA) is a well known and widely used formal model for the specification of such systems. While many methods exist for simulating hybrid automata, there are no known approaches for the automatic code generation from HA that are semantic preserving. If th…
▽ More
Hybrid systems are discrete controllers that are used for controlling a physical process (plant) exhibiting continuous dynamics. A hybrid automata (HA) is a well known and widely used formal model for the specification of such systems. While many methods exist for simulating hybrid automata, there are no known approaches for the automatic code generation from HA that are semantic preserving. If this were feasible, it would enable the design of a plant-on-a-chip (PoC) system that could be used for the emulation of the plant to validate discrete controllers. Such an approach would need to be mathematically sound and should not rely on numerical solvers. We propose a method of PoC design for plant emulation, not possible before. The approach restricts input/output (I/O) HA models using a set of criteria for well-formedness which are statically verified. Following verification, we use an abstraction based on a synchronous approach to facilitate code generation. This is feasible through a sound transformation to synchronous HA. We compare our method (the developed tool called Piha) to the widely used Simulink R simulation framework and show that our method is superior in both execution time and code size. Our approach to the PoC problem paves the way for the emulation of physical plants in diverse domains such as robotics, automation, medical devices, and intelligent transportation systems.
△ Less
Submitted 14 October, 2015;
originally announced October 2015.
-
A unified framework for modeling and implementation of hybrid systems with synchronous controllers
Authors:
Avinash Malik,
Partha Roop
Abstract:
This paper presents a novel approach to including non-instantaneous discrete control transitions in the linear hybrid automaton approach to simulation and verification of hybrid control systems. In this paper we study the control of a continuously evolving analog plant using a controller programmed in a synchronous programming language. We provide extensions to the synchronous subset of the System…
▽ More
This paper presents a novel approach to including non-instantaneous discrete control transitions in the linear hybrid automaton approach to simulation and verification of hybrid control systems. In this paper we study the control of a continuously evolving analog plant using a controller programmed in a synchronous programming language. We provide extensions to the synchronous subset of the SystemJ programming language for modeling, implementation, and verification of such hybrid systems. We provide a sound rewrite semantics that approximate the evolution of the continuous variables in the discrete domain inspired from the classical supervisory control theory. The resultant discrete time model can be verified using classical model-checking tools. Finally, we show that systems designed using our approach have a higher fidelity than the ones designed using the hybrid automaton approach.
△ Less
Submitted 23 January, 2015;
originally announced January 2015.
