dc.description.abstract |
In modern life, reactive systems are widely used in cyber-physical systems (CPS), such as airplanes and medical devices. One common characteristic of these systems is that they provide services by continuously interacting with our physical world. Thus, they often have strict requirements for functionality and timing. A system is classified as safety-critical if its malfunction may harm our well-being. Synchronous languages are ideally suited for designing safety-critical reactive systems. These languages provide guarantees on soundness such as determinism and reactivity of correct synchronous programs, which are known to be causal. Consequently, this allows the formal verification of functional properties and Worst-Case Reaction Time (WCRT). However, since the invention of the synchronous paradigm, there has been not many innovations regarding WCRT analysis. There has been only limited efforts to try and further both precision and scalability during these analyses, especially for programs involving a large number of threads. In addition, utilising power management in the synchronous paradigm, which is a key aspect for battery powered CPS, has received scant attention. In this thesis, we aim to address these shortcomings. WCRT analysis is essential for reactive systems, since they interact with our physical world. An output is considered correct if it is delivered in a timely manner. However, as the size of modern systems grow, existing techniques fail to deliver preciseWCRT estimates in a scalable manner. Our first attempt to solve this problem is presented in Chapter 3. We propose an iterative WCRT analysis called ILPC (ILP concurrent), based on Integer Linear Programming (ILP). ILP is conventionally known to be scalable, but produces pessimistic estimates. We discover that this is due to the abstraction of tick alignment in the ILP model, which trades precision for scalability. A key to achieve both precision and scalability is to incorporate the tick alignment but keep it separate from path analysis. In ILPC we divide WCRT analysis into two parts, and for each partwe develop suitable ILP based techniques. The proposed algorithm combines the two parts in an iterative manner to compute the WCRT. Our second attempt for scalable WCRT analysis is presented in Chapter 4, and it is based on explicit path enumeration. Conventional explicit path enumeration techniques include model checking and reachability analysis. A well-known problem of this approach is state explosion caused by the composition of concurrent threads. To tackle this problem, we develop a WCRT analysis technique called WCRT algebra, which is an adaptation of a min-max-plus algebra. We propose the idea of WCRT equivalence in modelling the control ow, and subsequently realise this as Tick Cost Automata (TCA). Using TCAs can effectively allow concurrent threads to be quickly composed without sacrificing precision. Both ILPc and WCRT algebra are benchmarked against the state-of-the-art published WCRT techniques using a set of industrial applications. The results show that both techniques are as precise as the existing techniques while being orders of magnitude faster in many instances. On average, ILPc is over 10 times faster than published WCRT techniques, and over 1000 times faster for large programs. WCRT algebra is about 3.5 time faster than ILPc. Finally, the last aspect this thesis tackles is the power management question for synchronous programs. While there are many exiting algorithms available for Real-Time Operating systems, they are not suited to the synchronous paradigm since they are tightly coupled with their adjoining schedulers. In Chapter 5, we propose a framework to combine Dynamic Voltage Frequency Scaling (DVFS) with the synchronous paradigm for the first time. Along with the framework, we develop a bi-criteria optimisation technique to automatically explore the trade-o s between timing and energy consumption using the concept of Pareto Optimality. We evaluate our approach against a conventional approach, where a single frequency is used throughout the execution. The results show that the proposed approach is able to produce more non-dominated options for the user providing more exibility. In conclusion, this thesis has pushed the boundary of the synchronous paradigm and opens new opportunities for its applications, especially for safety-critical CPS, which may have energy and timing constraints. |
en |