Synthesizing Architectural Models of Cyber-Physical Systems
Presented as part of the 2012 HCSS conference.
Abstract:
We show how to algorithmically synthesize architectural models of cyber-physical systems with hard real-time constraints. We do this by providing a meta-architectural specification language that allows designers to specify what properties their architectural models should have, not how to achieve them. This provides designers with a qualitatively new level of abstraction that enables the exploration of design spaces at the earliest stages of design, when doing so provides the most benefit. To solve the synthesis problem, we introduce the idea of Integer linear programming Modulo Theories (IMT). An IMT solver resembles an SMT (Satisfiability Modulo Theories) solver, except that instead of using a SAT solver at the core, we use an ILP (Integer Linear Programming) solver. We believe that the IMT approach has the potential to be widely applicable, as many practical problems from Operations Research and Engineering are routinely expressed using mathematical programming tools such as CPLEX. By allowing one to combine such problems with interesting background theories, the IMT approach has the potential to enable advances in a variety of areas, similar to those enabled in verification by SMT. We present our experiences in applying our work to Boeing's Dreamliner. Synthesizing architectural models for the Dreamliner required connecting and integrating numerous components that share resources, interact in complex, safety-critical ways, and have real-time constraints. The real-time constraint involve static cyclic scheduling, an industrially-relevant and particularly demanding type of real-time scheduling problem. We developed the CoBaSA tool, which is able to quickly and fully automatically synthesize architectures for the Dreamliner that satisfy all of the high-level constraints provided by Boeing.
Biography:
Dr. Pangiotis (Pete) Manolios is an Associate Professor in the College of Computer and Information Science at Northeastern University. Pete received his Ph.D. in Computer Sciences at the University of Texas at Austin in 2001.
Pete's main research interest is mechanized formal verification and validation of computing systems. What guides his research is the vision that formal methods can be used to revolutionize the design and implementation of highly reliable, robust, and scalable systems in a variety of important application areas, ranging from large component-based software systems to hardware systems to aerospace systems to computational biology to public health. Pete's other areas of interest include programming languages, distributed computing, logic, software engineering, algorithms, computer architecture, aerospace, and pedagogy.