CoBaSACoBaSA is a framework for synthesizing systems. It was used to successfully synthesize system architectures for Boeing's 787 (Dreamliner) and it was designed to be generally applicable.
MotivationThe motivation for this line of work was to address the complexity and cost associated with the design of safety-critical cyberphysical systems. The complexity of such cyberphysical systems, examples of which include ground, air, space, and sea vehicles, has been increasing at an exponential rate, independent of any reasonable metric used. These systems tend to be distributed and consist of numerous interconnected components that share resources, interact in complex, safety-critical ways, and have real-time constraints. The design, implementation, and maintenance of such systems is a major challenge and there is wide consensus that the design of complex systems requires raising the level of discourse by utilizing abstraction, in particular high-level modeling. For example, Boeing's 787 Dreamliner consists of thousands of interacting components, and just the software enabling fly-by-wire control is over 10 million lines of code. To design such complex systems, numerous models at various levels of abstraction are used, with one of the highest levels being at the system architecture. At this level, the focus is on structural properties of the system and component interactions. While many architecture description languages have been proposed, these languages require users to specify what components are to be used and how they are to be connected. The effort required to do this can be significant. According to Boeing, during the design of the 787 Dreamliner, the construction of the architectural models for required the "cooperation of multiple teams of engineers working over long periods of time." We developed the CoBaSA (Component-Based System Assembly) framework to algorithmically synthesize architectural models using the actual production design data and constraints arising during the development of the Dreamliner. CoBaSA provides a high-level modeling and specification language, coupled with a synthesis tool based on verification and optimization technology. While the previous methods for creating architectural models required significant iteration between multiple teams working over long periods of time, we were able to automatically synthesize architectures in minutes directly from the high-level requirements. This allows designers to specify what they want, not how to achieve it.
A list of papers related to CoBaSA are provided below, as are links to the publicly available tools we have developed. While the papers are listed in chronological order, I would recommend reading the ISSTA 2007 paper (our first paper on the topic) followed by the CAV 2011 paper (which describes the full Boeing problem and how we solved it), followed by the CAV 2013 paper (which describes our IMT framework, a new framework for combining decision procedures where a MILP solver is used as a core engine instead of a SAT solver). The CAV 2007, ICCAD 2006, SAT 2007, DATE 2009, and FMCAD 2011 papers describe some of the verification technology we developed while chasing a solution to the architectural synthesis problem. The AVICPS 2010 paper describes the class of constraints associated with system architectures based on our experience with the Dreamliner.
We have demonstrated that algorithmic synthesis of system architectures is possible for complex cyberphysical systems. There are many intersting next steps. The first is to go from a one-off success to wide industry adoption. This involves showing how to integrate this kind of technology into the design cycle, how to use this technology for design exploration, and how to use it for certification credit. Another direction is to explore how this technology can be used to address problems in other fields, such as big data.
ToolsMy research team has developed several versions of CoBaSA. The latest such tool is called "inez". Inez was developed by my student Vasilis Papavasileiou. Previous versions of CoBaSA are not available.
- Inez is a constraint solver that implements the ILP Modulo Theories (IMT) scheme, as described in our CAV 2013 paper. We have used the IMT approach to solve industrial synthesis and design problems with real-time constraints arising in the development of the Boeing 787. Inez can be used to solve problems involving linear constraints and optimization. Inez is OCaml-centric. The preferred mode of interacting with the solver is via scripts written in a Camlp4-powered superset of OCaml.
- Panagiotis Manolios, Jorge Pais and Vasilis Papavasileiou.
The Inez Mathematical Programming Modulo Theories Framework.
CAV, Computer-Aided Verification (CAV 2015)
- Panagiotis Manolios, Vasilis Papavasileiou, and Mirek Riedewald.
ILP Modulo Data. FMCAD, Formal Methods in Computer-Aided Design (FMCAD 2014)
- Panagiotis Manolios and Vasilis Papavasileiou. ILP Modulo Theories. CAV, 2013. Springer.
- Panagiotis Manolios and Vasilis Papavasileiou. Pseudo-Boolean Solving by Incremental Translation to SAT. FMCAD, 2011. Springer.
- Christine Hang, Panagiotis Manolios, and Vasilis Papavasileiou. Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints. CAV, 2011. Springer.
- Panagiotis Manolios and Vasilis Papavasileiou. Virtual Integration of Cyber-Physical Systems by Verification. AVICPS, 2010.
- Benjamin Chambers, Panagiotis Manolios, and Daron Vroon. Faster SAT Solving with Better CNF Generation. DATE 2009, Design Automation and Test in Europe, April 2009. IEEE.
- Panagiotis Manolios. Automating the Assembly of Avionics Systems. AIAA Guidance, Navigation, and Control Conference. August 2008. (Invited)
- Panagiotis Manolios. Automating System Assembly of Aerospace Systems. The Sixth NASA
Langley Formal Methods Workshop, April 2008.
- Panagiotis Manolios, Sudarshan Srinivasan, and Daron
Vroon. BAT: The Bit-Level Analysis Tool.
CAV 2007, Nineteenth International on Computer Aided Verification. July 2007.
- Panagiotis Manolios, Gayatri Subramanian, and Daron Vroon.
Automating Component-Based System Assembly.
ISSTA 2007, International Symposium on Software
Testing and Analysis. July 2007.
- Panagiotis Manolios and Daron Vroon.
Efficient Circuit to CNF Conversion.
SAT 2007, The Tenth International Conference on Theory
and Applications of Satisfiability Testing. May 2007.
- Panagiotis Manolios, Sudarshan K. Srinivasan, and Daron Vroon. Automatic Memory Reductions for RTL-Level Verification. ICCAD 2006, ACM-IEEE International Conference on Computer Aided Design, November 2006.