Compositional Real-Time Analysis for Cyber-Physical Systems
Date: April 16, 2012
Venue: Friendship Hotel in Beijing, China
Linh Thi Xuan Phan, University of Pennsylvania (linhphan[at]cis.upenn.edu)
Insup Lee, University of Pennsylvania (lee[at]cis.upenn.edu)
Insik Shin, KAIST, Korea (insik.shin[at]cs.kaist.ac.kr)
Oleg Sokolsky, University of Pennsylvania (sokolsky[at]cis.upenn.edu)
This tutorial is concerned with various aspects of component-based design and compositional analysis of cyber-physical systems, with a focus on timing issues. It will first give an overview of component-based frameworks and their underlying principles. It will then go in-depth into abstraction methods for real-time components and techniques for computing their optimal interfaces, for both systems implemented on uniprocessor and multiprocessor platforms, as well as extensions to multi-mode systems. Besides theoretical aspects, the tutorial will also present an architectural platform support for compositional scheduling based on Xen virtualization and a demonstration of the CARTS toolset with several examples seeing the techniques in action. It will also include two case studies highlighting the utility of the framework, including the ARINC-653 avionics software and a smart-phone application. We will conclude the tutorial with open challenges and research opportunities in this domain.
Real-time interfaces, Compositional schedulability analysis, Hierarchical scheduling, Multi-mode systems
Cyber-physical systems (CPS) are physical and engineered systems whose operations are monitored, coordinated, controlled and integrated by computing and communication cores. Tomorrow's CPS is expected to embed cyber capabilities in every physical process and component (e.g., brakes and engines of vehicles) and employ networking at multiple and extreme scales. The resulting systems-of-systems are highly networked and dynamic in nature, with increasing time-critical interactions between purely physical elements and intangible cyber elements. This exponential growth in complexity of CPS has brought forward an extensive adoption of component-based design approaches using components' interfaces.
In the context of CPS, software components are typically implemented on a shared set of hardware resources under a certain scheduling policy, and each component may employ a different local resource sharing policy for its subcomponents. Consequently, an interface must encapsulate not only the functional aspects but also the resource requirements of the underlying components. Accurate and efficient interface generation and composition are therefore crucial to guarantee correct timing behavior of CPS constructed using the component-based approach. This tutorial will provide a comprehensive overview of recent developments in this domain, and it will highlight several remaining open issues and research opportunities.
Motivating example: A running example that will be used to illustrate the concepts and techniques in the tutorial.
Compositional analysis basics: Introduction to compositional analysis of hierarchical scheduled systems and its role in the component-based development; notions of resource interfaces; key desirable properties.
Real-time scheduling background: Standard real-time task models (e.g., periodic, sporadic), schedulability analysis of common scheduling policies (e.g., Earliest Deadline First, Deadline Monotonic) based on demand/supply bound analysis and worst-case response time analysis, which will serve as basic foundation for compositional analysis.
Resource interfaces: Different interface representations of components' resource requirements (e.g., periodic resource models, explicit deadline periodic resource models).
Interface computation techniques: Notions of optimal interfaces; techniques for generating optimal interfaces; interface composition techniques, for both general and special cases (e.g., harmonic task periods, offset-aligned components).
Extensions to multiprocessor platforms: Virtual cluster-based multiprocessor scheduling; resource interfaces for virtualized multiprocessor platforms; optimal interface generation techniques.
Extensions to multi-mode systems: Characteristics and challenges of multi-mode systems; mode-change protocols; multi-mode automata models; interface automata for multi-mode systems; multi-mode compositional analysis.
Tools and architecture support: An introduction to the CARTS toolset for compositional analysis and the real-time virtual machine monitor RT-Xen.
Demonstration: ARINC-653 avionics software and smart-phone application case studies.
Challenges and opportunities: Open issues and research opportunities in real-time compositional analysis as well as its integration to existing functional component-based frameworks, from both theoretical and practical perspectives.
The level of the tutorial will be from introductory to intermediate. It will especially appeal to an audience who is familiar with timing analysis and scheduling of closed systems and is interested in how to extend to compositional analysis and open systems, or an audience who is knowledgeable of component-based development and would like to extend them to incorporate timing aspects. However, the tutorial is self-contained and assumes no background in timing analysis or component-based development. The material to be presented will be useful to researchers, students, software designers and developers working or planning to work in the real-time embedded systems and cyber-physical systems domains.
Linh T.X. Phan is a Postdoctoral Researcher in the PRECISE Center at the University of Pennsylvania. She received the B.S. degree in Computer Science in 2003 and the Ph.D. degree in Computer Science in 2009 from the National University of Singapore (NUS). Her research interests include formal modeling and analysis methods, system-level design techniques, and compositional analysis methods for real-time embedded systems, cyber-physical systems and multi-mode systems. Some of the application domains she works in include automotive electronics and software, avionics, real-time multimedia, body-area sensor networks and cloud computing. She was a recipient of the Singapore Scholarship (1999--2003) and NUS Graduate Scholarship (2003--2007). For her Ph.D. dissertation, she received the Graduate Research Excellence Award from NUS (2009). She also received the Best Paper Award nomination at EMSOFT 2010. She has served as a co-chair of APRES 2011 and CRTS 2011, and a PC member of ETFA 2010--2011, EMC 2010--2011, CRTS 2010--2011, RTAS WiP 2010--2012, CPSNA 2011, WTR 2011, and WCTT 2011.
Insup Lee is the Cecilia Fitler Moore Professor of Computer and Information Science and Director of PRECISE Center at the University of Pennsylvania. He also holds a secondary appointment in the Department of Electrical and Systems Engineering. He received the B.S. degree in mathematics from the University of North Carolina, Chapel Hill, and the Ph.D. degree in computer science from the University of Wisconsin, Madison.
His research interests include cyber physical systems, real-time systems, embedded and hybrid systems, formal methods and tools, high-confidence medical device systems, and software engineering. The theme of his research activities has been to assure and improve the correctness, safety, and timeliness of life-critical embedded systems. His paper with his student on compositional schedulability analysis received the best paper award in RTSS 2003.
He was Chair of IEEE Computer Society Technical Committee on Real-Time Systems (2003--2004) and an IEEE CS Distinguished Visitor Speaker (2004--2006). He has served on many program committees and chaired several international conferences and workshops, including IEEE RTSS, IEEE RTCSA, IEEE ISORC, CONCUR, ACM EMSOFT, ACM/IEEE ICCPS, and HCMDSS/MD PnP. He has also served on various steering and advisory committees of technical societies, including CPSWeek, ESWeek, ACM SIGBED, IEEE TC-RTS, RV, ATVA. He has served on the editorial boards on the several scientific journals, including IEEE Transactions on Computers, Formal Methods in System Design, and Real-Time Systems Journal. He is a founding co-Editor-in-Chief of KIISE Journal of Computing Science and Engineering (JCSE) since Sept 2007. He was a member of Technical Advisory Group (TAG) of President's Council of Advisors on Science and Technology (PCAST) Networking and Information Technology. He is IEEE fellow and received IEEE TC-RTS Technical Achievement Award in 2008.
Insik Shin is an assistant professor in the Dept. of Computer Science at KAIST since 2008. He received a B.S. from Korea University and an M.S. from Stanford University both in Computer Science in 1994 and 1998 respectively. He received a Ph.D. from University of Pennsylvania in 2006 on Compositional Schedulability Analysis in Real-Time Embedded Systems. He has been a post-doctoral research fellow at Malardalen University, Sweden, and a visiting scholar at University of Illinois, Urbana-Champaign until 2008.
His research interests lie in cyber-physical systems and real-time embedded systems. His papers on compositional schedulability analysis received the Best Paper award from IEEE Real-Time Systems Symposium (RTSS) in 2003 and were nominated for the Best Paper award at IEEE ECRTS and IEEE RTSS in 2008, respectively. His paper also received the Best Student Paper award from IEEE RTAS in 2011. He has been a co-founding chair of a workshop (CRTS) in 2008 and will be a co-chair of the CPSNA workshop in 2012. He has also served various program committees in real-time embedded systems, including RTSS, RTAS, ECRTS, EMSOFT, RTCSA, and ETFA.
Oleg Sokolsky received M.Sc in Computer Science from St. Petersburg Technical University (Russia) in 1988 and Ph.D. in Computer Science from SUNY at Stony Brook in 1996. Oleg Sokolsky is a Research Associate Professor at the University of Pennsylvania, where he has occupied research staff positions since 1998. His research interests include formal methods for the modeling and analysis of real-time and hybrid systems, model checking, and formal monitoring and run-time checking. He has published over 40 research articles in these areas. He has been one of the primary developers of the CHARON toolkit, as well as a number of other modeling and analysis tools. Before joining the University of Pennsylvania, Dr. Sokolsky worked as a Computer Scientist at the Computer Command and Control Company in 1996-1998, where he was the Principal Investigator on an SBIR contract funded by ONR.Dr. Sokolsky is serving on the Steering Committee of the Conference on Runtime Verification and was the Program Chair of this conference in 2010. He also served as the Program Chair (2005), General Chair (2006), and Finance Chair (2007) of the IEEE RTAS and as the Design and Verification track Chair at the RTSS in 2009. He also organized several workshops in the domain of real-time and embedded systems, including Run-time Verification (2003, 2007), Innovative Technologies for the Certification of Embedded Systems (2006), Composition of Real-Time Systems (2008,2009), and Composition of Embedded Systems (2006). He has served on the program committees of conferences in the area of real-time and embedded systems, including the IEEE RTSS (2002,2005--2010) and IEEE RTAS (2002, 2004, 2007, 2008, 2010), IEEE RTCSA (2005--2007), IEEE ISORC (2000, 2002, 2004, 2008, 2009), ECRTS (2006 and 2010).