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.
Gustavo Carvalho
Gustavo Carvalho
Lecturer @ CIn-UFPE (BR)

My research interests include formal specification/verification, and tools development.