Semi-Automated Design Space Exploration for Formal Modelling

TL;DR

This paper introduces a semi-automated approach to assist designers in formal system modeling by exploring various design alternatives using automated reasoning and theory formation techniques, aiming to improve abstraction and fault analysis.

Contribution

It presents a novel Design Space Exploration method that combines modeling patterns with automated reasoning to guide formal model development in real-time.

Findings

Provides high-level modeling guidance automatically

Explores multiple design alternatives efficiently

Proposes models that effectively handle faults

Abstract

Refinement based formal methods allow the modelling of systems through incremental steps via abstraction. Discovering the right levels of abstraction, formulating correct and meaningful invariants, and analysing faulty models are some of the challenges faced when using this technique. Here, we propose Design Space Exploration, an approach that aims to assist a designer by automatically providing high-level modelling guidance in real-time. More specifically, through the combination of common patterns of modelling with techniques from automated theory formation and automated reasoning, different design alternatives are explored and suitable models that deal with faults are proposed.