Hybrid systems are a subset of Cyber-Physical System (CPS), where a physical process (the plant) is controlled by a discrete controller. The controller induces mode switches, which are modelled as guard conditions leading to sudden discontinuities. Correctly capturing sudden discontinuities during simulation is the primary challenge to maintain fidelity. De-facto industry standard tools, such as Simulink and Modelica, have been known to produce incorrect outputs when simulating systems involving complicated guards. For example, transcendental guards leading to the well-known even number of level crossing detection problem or guards leading the system state into the complex plane have been shown to produce invalid results. To tackle this problem we propose Higher Order Hybrid Automata and its compositional execution semantics. Using this semantics a novel numerical simulation approach for hybrid systems is developed. The key idea is to approximate the guard and Ordinary Differential Equations with Taylor polynomials so as to accurately detect zero-crossings induced by the guards. Simulation results show that systems with transcendental guards can be simulated using our approach efficiently, while maintaining high simulation fidelity.

Rear-end collision avoidance relies on mathematical models to calculate the safety distance. Vehicle deceleration is a key parameter for the accuracy of the models. Current models, however, assume a constant deceleration during braking, which is unrealistic. This assumption results in large over-approximation / under-approximation. In this paper, we rectify this limitation by proposing a new model that accounts for realistic vehicle deceleration during braking. Simulation results show that our approach guarantees safety. Moreover, traffic flow is improved by 21.6% compared to the widely adopted the Berkeley algorithm.

Real-time systems are designed using model-driven approaches, where a complex system is represented as a set of interacting components. Such a compositional approach facilitates design of simpler components, which are easier to validate and integrate with the overall system. In contrast to such systems, data-driven systems like neural networks are designed as monolithic black-boxes to capture the non-linear relationship from inputs to outputs. Increasingly, such systems are being used in safety-critical real-time systems. Here, a compositional approach would be ideal. However, to the best of our knowledge, such a compositional approach is lacking while designing data-driven components based on neural networks.This paper formalises this problem by developing the concept of Composed Neural Networks (CpNNs) by extending the well known Keras python framework. CpNNs formalise the synchronous composition of several interacting neural networks in Keras. Further, using the developed semantics, we enable modular compilation from a given CpNN to C code. The generated code is suitable for the Worst-Case Execution Time (WCET) analysis. Using several benchmarks we demonstrate the superiority of the developed approach over a recently proposed approach using Esterel, as well as the popular Python package Tensorflow Lite. For the given benchmarks, our approach is superior to Esterel with an average WCET reduction of 64.06%, and superior to Tensorflow Lite with an average measured WCET reduction of 62.08%.

Cyber-Physical Systems are highly safety critical, especially since they have to provide both functional and timing guarantees. Increasingly, Cyber-Physical Systems such as autonomous vehicles are relying on Artificial Neural Networks in their decision making and this has obvious safety implications. While many formal approaches have been recently developed for ensuring functional correctness of machine learning modules involving Artificial Neural Networks, the issue of timing correctness has received scant attention.

Simulink/Stateflow® is the de-facto tool for design of Cyber-physical Systems (CPS). CPS include hybrid systems, where a discrete controller guides a continuous plant. Hybrid systems are characterised by their continuous time dynamics with sudden discontinuities, caused by level/zero crossings. Stateflow can graphically capture hybrid phenomenon, making it popular with control engineers. However, Stateflow is unable to correctly and efficiently simulate complex hybrid systems, especially those characterised by even number of level crossings.

Car-following is the activity of safely driving behind a leading vehicle. Traditional mathematical car-following models capture vehicle dynamics without considering human factors, such as driver distraction and the reaction delay. Consequently, the resultant model produces overly safe driving traces during simulation, which are unrealistic. Some recent work incorporate simplistic human factors, though model validation using experimental data is lacking. In this paper, we incorporate three distinct human factors in new compositional car-following model called modal car-following model, which is based on hybrid input output automata (HIOA). HIOA have been widely used for the specification and verification of cyber-physical systems. HIOA incorporate the modeling of the physical system combined with discrete mode switches, which is ideal for describing piece-wise continuous phenomena. Thus, HIOA models offer a succinct framework for the specification of car-following behavior. The human factors considered in our approach are estimation error (due to imperfect distance perception), reaction delay, and temporal anticipation. Two widely used car-following models called Intelligent Driver Model (IDM) and Full Velocity Difference Model (FVDM) are used for extension and comparison purpose. We evaluate the root mean square (rms) error of the following vehicle position using the traces obtained from human drives through different driving scenarios. The result shows that our model reduces the rms error in IDM and FVDM by up to 48.8% and 7.41%, respectively.

In wireless networks, a message is dropped unexpectedly due to the physical phenomena such as fading, thus requiring a number of backup retransmissions. However, retransmission (which is known to be probabilistic) is mostly disabled in the design of time-triggered communication by the precomputed schedule that reserves every transmission tightly. In this paper, we formally specify the scheduling constraints for a time-triggered wireless network to account for retransmissions in the schedule. We use analytic models of radio propagation to predict the number of retransmissions needed to achieve the desired probability of receiving a packet. Then, the schedule is generated by solving the scheduling constraints by using a Satisfiability Modulo Theory (SMT) solver. We verify the correctness of the resulting schedule to show that our constraints can produce a correct schedule. The performance of the schedule synthesis with different network sizes, topologies, and the number of transmissions are evaluated.

We propose a model-driven approach for designing Wireless Sensor Network (WSN) applications, specifically for systems where hard real-time requirements must be satisfied. Traditionally, developing such systems presents difficulties in ensuring time and timing accuracy due to unpredictable computation time, ambiguities in program concurrency, and behavioural inconsistency between model and implementation. However, in contrast, the models in our approach are fully time-predictable by means of a logical time interval called a tick, while concurrency is automatically handled by the design semantics in a timing guaranteed manner. Meanwhile, the model-driven aspect of automatic code generation guarantees the behavioural consistency between model and implementation. We achieve our approach by using IEC 61499 function blocks and synchronous execution for syntax and semantics respectively. In this paper, we design a time-triggered protocol and a distributed motor synchronization as the network and application layers respectively. Then, we model the overall system for validation by performing composition of such layers. Furthermore, we explain how the logical time tick can be realized during the implementation in a way that the real-time requirement can be satisfied. Finally, the simulation and implementation results demonstrate the effectiveness of our approach.