System development is a dynamic and iterative process that involves refinements and revisions, often resulting in some components being only partially specified. To ensure that the system meets its requirements is essential to have the ability to perform continuous verification after each refinement or revision step. This calls for both models and verification techniques that can effectively handle incompleteness.
In this presentation, I will introduce incomplete models and model-checking techniques designed to address such models. Furthermore, I will show how these techniques can support other steps in the software development lifecycle, including requirements elicitation, design, and specification mining.