TUTORIAL DESCRIPTION

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.

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 on parallel and multi-core platforms. 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 in FRP.

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 multi-resources.

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.

Albert M. K. Cheng is Full Professor and former interim Associate Chair of the Computer Science Department at the University of Houston (UH). His research interests center on the design, specification, modeling, scheduling, and formal verification of real-time, embedded, and cyber-physical systems, green/power/thermal-aware computing, software engineering, knowledge-based systems, and networking. He is the founding Director of the UH Real-Time Systems Laboratory. He received the B.A. with Highest Honors in Computer Science, graduating Phi Beta Kappa at age 19, the M.S. in Computer Science with a minor in Electrical Engineering at age 21, and the Ph.D. in Computer Science at age 25, all from The University of Texas at Austin, where he held a GTE Foundation Doctoral Fellowship. He has served as a consultant for many organizations, including IBM and Shell, and was also a Visiting Professor in the Departments of Computer Science at Rice University and the City University of Hong Kong.

Dr. Cheng is the author/co-author of over 240 refereed publications in leading journals (including IEEE Transactions on Computers, IEEE Transactions on Software Engineering, and IEEE Transactions on Knowledge and Data Engineering) and top-tier conferences (including RTSS, RTAS, ICPADS, ISLPED, LCN, and PADL), and has received numerous awards, including the U.S. National Science Foundation Research Initiation Award (now known as CAREER) and the Texas Advanced Research Program Grant (ranking 12th among 373 funded proposals). He has been invited to present seminars, tutorials, panel positions, and keynotes at over 100 conferences, organizations, and universities (most recently at the University of Toronto, SEI/Carnegie Mellon University, TU Wien, Caltech, University of California at Berkeley, University of Washington, Sapienza University of Rome, University of Oxford, INRIA, University of British Columbia, UT-Austin, and Columbia University). He is and has been on the technical program committees (including many program chair positions) of over 280 conferences, symposia, workshops, and editorial boards (including the IEEE Transactions on Software Engineering 1998-2003 and the IEEE Transactions on Computers 2011-2015). He is Guest Co-Editor of a 2013 Special Issue on Rigorous Modeling and Analysis of Cyber-Physical Systems of the IEEE Embedded Systems Letters, Guest Editor of the 2014-2015 and 2016 Special Issues on Cyber-Physical Systems of SENSORS, and Guest Co-Editor of a 2016 Special Issue on Real-Time Scheduling on Heterogeneous Multi-core Processors of Microprocessors and Microsystems (MICPRO) - the Elsevier Embedded Hardware Design Journal. He has been the Program Co-Chair of the 2013 IEEE International Conference on Service Oriented Computing and Applications (SOCA) and Program Co-Chair of the System, Models and Algorithms Track of the 2014 IEEE International Conference on Embedded Software and Systems (ICESS), where he delivered an award-winning Keynote.

REFERENCES

[2] S. Andrei and A. M. K. Cheng, "Efficient Verification and Optimization of Real-Time Logic Specified Systems," IEEE Transactions on Computers, vol. 58, no. 12, pp. 1640-1653, December 2009.

[3] Chaitanya Belwal and Albert M. K. Cheng, "Determining Actual Response Time in P-FRP," ACM International Symposium on Practical Aspects of Declarative Languages (PADL), Austin, Texas, USA January 2011.

[4] Albert M. K. Cheng, Homa Niktab, and Michael Walston, "Timing Analysis of Small Aircraft Transportation System (SATS)," IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Seoul, Korea, August 2012.

[5] Yong woon Ahn and Albert M. K. Cheng, "Automatic Resource Scaling for Medical Cyber-Physical Systems Running in Private Cloud Computing Architecture," Medical Cyber Physical Systems Workshop (MedicalCPS), Cyber-Physical Systems Week (CPSWeek), Berlin, Germany, April 14, 2014.

[6] Yu Li and Albert M. K. Cheng, "Transparent Real-Time Task Scheduling on Temporal Resource Partitions," IEEE Trans. on Computers, May 2016.

[7] Xingliang Zou, Albert M. K. Cheng, and Yu Jiang, "A Non-Work-Conserving Model for P-FRP Fixed Priority Scheduling," 13th IEEE International Conference on Embedded Software and Systems (ICESS), Chengdu, China, August 13-24, 2016.

[8] Xingliang Zou, Albert M. K. Cheng, Carlos Rincon and Yu Jiang, "Multi-Mode P-FRP Task Scheduling," 20th IEEE Intl. Symp. Real-time Computing (ISORC), Toronto, Canada, May 2017. Outstanding Paper Award.

[9] Zeinab Kazemi and Albert M. K. Cheng, "A Scratchpad Memory-Based Execution Platform for Functional Reactive Systems and its Static Timing Analysis," 22nd IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), Daegu, Korea, August 17-19, 2016.

Functional reactive programming (FRP) [3,7,8,9]

Response time analysis - Part 1 [3,7,8,9]

Response time analysis - Part 2 [3,7,8,9]

Formal analysis & verification techniques based on Real-Time Logic (RTL) [2]

Real-Time Virtual Resources (RTVR) on multi-core platforms [6]

Case studies of actual systems [4,8,9]