Playing with State-Based Models for Designing Better Algorithms
Résumé
State-based models provide a very convenient framework for analysing, verifying, validating and designing sequential as well as concurrent or distributed algorithms. Each state-based model is considered as an abstraction, which is more or less close to the target algorithmic entity. The problem is then to organise the relationship between an initial abstract state-based model expressing requirements and a final concrete state- based model expressing a structured algorithmic state-based model. A simulation (or refinement) relation between two state-based models allows to structure these mod- els from an abstract view to a concrete view. Moreover, state-based models can be extended by assertion languages for expressing correctness properties as pre/post spec- ification, safety properties or even temporal properties. In this work, we review state- based models and play scores for verifying and designing concurrent or distributed algorithms. We choose the Event-B modelling language for expressing state-based models and we show how we can play Event-B scores using Rodin and methodologi- cal elements to guarantee that the resulting algorithm is correct with respect to initial requirements. First, we show how annotation-based verification can be handled in the Event-B modelling language and we propose an extension to handle the verification of concurrent programs. In a second step, we show how important is the concept of refinement and how it can be used to found a methodology for designing concurrent programs using the coordination paradigm.