A model-based framework for compositional verification and testing of reactive systems | Current Project

This project proposes an integrated framework for the verification and testing of reactive systems.

The framework is based on the Model-Driven Engineering (MDE) methodology and it is compositional; the verification and testing of complex systems reuses the analyses performed with respect to the system components. The compositional approach is essential for achieving scalability, a typical challenge for formal verification. As input, we consider models in SysML, but also textual specifications in a controlled natural language.