M04 System Development and Verification | Developing Next-Generation Embedded Systems: Functional Reactive Programming, Formal Verification, and Real-Time Virtual Resources

Organiser:
Albert M. K. Cheng, University of Houston, Texas, US

The use of sophisticated digital systems to control complex physical components in real-time has grown at a rapid pace. These applications range from traditional stand-alone systems to highly-networked cyber-physical systems (CPS), spanning a diverse array of software architectures and control models. Examples include city-wide traffic control, robotics, medical systems, autonomous vehicular travel, green buildings, physical manipulation of nano-structures, and space exploration. Since all these applications interact directly with the physical world and often have humans in the loop, we must ensure their physical safety. Obviously, the correctness of these embedded systems and CPSs depends not only on the effects or results they produce, but also on the time at which these results are produced. For instance, in a CPS consisting of a multitude of vehicles and communication components with the goal to avoid collisions and reduce traffic congestions, formal safety verification and response time analysis are essential to the certification and use of such systems - all described in this tutorial.

Organiser:
Albert M. K. Cheng, University of Houston, Texas, US

The benefits of using the functional (reactive) programming (FRP) over the imperative programming style found in languages such as C/C++ and Java for implementing embedded and real-time software are several. The functional programming paradigm allows the programmer to intuitively describe safety-critical behaviors of the system and connect its components, thus lowering the chance of introducing bugs in the design phase. Its stateless nature of execution does not require the use of synchronization primitives like mutexes and semaphores, thus reducing the complexity in programming. Hence, FRP can potentially transform the way we implement next-generation embedded systems and CPS. However, accurate response time analysis of FRP-based controllers remains a largely unexplored problem. The first part of this tutorial will introduce a framework for accurate response time analysis, scheduling, and verification of embedded controllers implemented as FRP programs.

Conclusion of the introduction to Functional reactive programming (FRP) and its Response time analysis.

Organiser:
Albert M. K. Cheng, University of Houston, Texas, US

This session introduces RTL (real-time logic)-based specification, formal verification, and debugging of real-time, embedded, and CPS. We have developed a fast approach for the verification and debugging of RTL-specified timing constraints: counting the truth assignments (incremental counting satisfiability) instead of traditional Boolean satisfiability. This metric can also indicate how far away a given specification (SP) is from satisfying its safety assertion (SA). The goal is to apply this technique to actual code and entire embedded systems. We present a framework to optimize these systems by automatically relaxing SP or tightening SA. We also present a faster verification technique for RTL-specified systems via decomposition and extended the path-RTL class to a larger class amenable to efficient analysis. This compositional approach to verification/analysis can be applied to optimization. We have discovered an even larger class of polynomial-time-analyzable RTL formulas called Linear RTL. Our technique can significantly speed-up the testing of combinational circuits. This session presents the RTL-based timing analysis of the Small Aircraft Transportation System (SATS) and the NASA X-38 Crew Return Vehicle Avionics. Our work has been a Featured Article of the IEEE Transactions on Computers.

Organiser:
Albert M. K. Cheng, University of Houston, Texas, US

Real-time resource partitioning (RP) divides hardware resources (processors, cores, and other components) into temporal partitions and allocates these partitions as virtual resources (physical resources at a fraction of their service rates) to application tasks. RP can be a layer in the OS or firmware directly interfacing the hardware, and is a key enabling technology for virtualization and cloud computing. Open embedded systems make it easy to add and remove software applications as well as to increase resource utilization and reduce implementation cost when compared to systems which physically assign distinct computing resources to run different applications. The second part of this tutorial will describe ways to maintain the schedulability of real-time tasks as if they were scheduled on dedicated physical resources and increase the utilization of the physical resources.