Compositional Abstraction and Refinement for Aspects (CARA)
John Rushby · 2004
The project originally focused on compositional formal methods for aspect-oriented programs and was located in the PCES program. Soon after its inception, however, the project was moved to the SEC (Software Enabled Control) program where its focus shifted to formal analysis of mixed discrete/continuous (i.e., hybrid) systems. We developed a two-step approach to analysis of hybrid systems: compute a property-preserving discrete approximation to the original hybrid system, and then analyze the discrete approximation. The approximation method is called Hybrid Abstraction and was developed by us in the DARPA MoBIES program. In the present project, we developed the theorem-proving technology that enables automated calculation of the approximation, and we built the SAL (Symbolic Analysis Laboratory) system for specification and analysis of discrete systems.