Compositional modelling, verification and testing of systems with applications in the aerospace industry | Concluded in 2018

In this project, we propose the systematisation of various aspects of the development of complex systems, particularly, with an emphasis on Systems of Systems (SoS).

The project scope includes modelling (semiformal and formal), verification (formal analysis of properties of interest), and testing of such systems. We use SysML to describe requirements and models of SoSs. SysML models are translated (automatically) into Circus models. Circus combines the process algebra CSP, to express reactive aspects, the language Z, to express data, and Dijkstra’s notation of guarded commands. With the support of Embraer, it is also part of the project’s scope an industrial evaluation of the proposed modelling, verification and testing strategies.