Context
Over the last twenty years, model-based design has become standard practice in fields such as automotive, aerospace engineering, and systems and synthetic biology. Formal methods, like temporal logics and model checking, allow a precise description and automatic verification of a prototype's requirements.
The rise of cyber-physical systems pushes complexity further and opens new challenges:
- standard temporal logics cannot express every kind of requirement designers need, for example non-functional requirements;
- standard model checking cannot cope with this level of complexity, because of the state space explosion.
Contributions
The thesis uses machine learning, active learning and optimisation to address these challenges:
- Signal measure logic, a new temporal logic suited to non-functional requirements (see also Signal Convolution Logic);
- evolutionary algorithms and Signal Temporal Logic for a supervised classification problem (see A robust genetic algorithm);
- a system design problem with multiple conflicting requirements (see Logic-based multi-objective design).