Building Correct by Construction Hard Real-Time Safety Critical Globally Asynchronous Locally Synchronous Software Systems

Abstract

Most of today’s embedded systems are very complex. With decreasing hardware costs and rapidly developing semiconductor fabrication technology, designers are now able to build systems that incorporate a wide variety of computing technologies, the so called Cyber-Physical Systems (CPS). These systems, controlled by computer programs, continuously interact with their physical environments through a network of sensory input and output devices. Consequently, the operations of such embedded systems are highly reactive and concurrent. Since embedded systems are deployed in many safety-critical applications, where failures can lead to catastrophic events, an interdisciplinary approach such as mathematical logic and formal verification is employed in order to ensure correct behaviour of the control algorithm. The size of these embedded applications is growing significantly each year. With increased time-to-market pressure, automatic and verified code generation from a design described in a high-level language is becoming of utmost importance. There has been significant effort in the development of a reactive programming language called SystemJ, which is based on the Globally Asynchronous Locally Synchronous (GALS) Model of Computation (MOC). With SystemJ, designers can describe a system using a number of asynchronously running concurrent processes called clock-domains. Each clock-domain is hierarchically composed of one or more reactions, which run concurrently but in lock-step with respect to the speed of the clock-domain. Reactions within a clock-domain communicate through broadcast based communication mechanism, while reactions in two different clock-domains communicate using a message passing mechanism. Similar to other reactive languages, SystemJ is designed based on formal mathematical semantics, allowing one to reason about the designed system before deployment. However, there have been very few studies on verification of programs developed in SystemJ and its GALS language counterparts, which makes it difficult to persuade designers to use such languages in practice. In this thesis, we propose an approach to close this gap by introducing a safety-critical subset of SystemJ called Safety-Critical SystemJ (SC-SystemJ) so that designers are able to automatically verify functional and real-time properties of the GALS system they develop with the language. The original SystemJ language has been refined in order to make it amenable to both functional and real-time property verification. In particular, the SC-SystemJ semantics is based on big-step, which enables translating of the program into a network of finite state machines (FSM). The program can then be verified using many available and wellestablished techniques, which are based on automata theories. With the proposed approach, designers can verify functional correctness of the system on the generated FSMs, which is also an input for back-end code generation, thereby facilitating the What You Prove Is What You Execute (WYPIWYE) paradigm. In addition, an SMT based real-time analysis of the system has been introduced, which verifies whether the system, consisting of multiple communicating clock-domains, will generate output event(s) in response to input event(s) within certain time bounds as specified by the designer. Finally, a novel real-time programming technique has been introduced to the SC-SystemJ language via exact and non-exact real-time waits, which allows designers to describe real-time delays in the program behaviour like in traditional programming languages without need of external timers. Lastly, in order to support the new semantics as well as functional and real-time property verification, a tool-chain for the verification of the SC-SystemJ language has been developed, which includes the compiler, enabling correct-by-construction (WYPIWYE) design process.