Skip to Main content Skip to Navigation
Journal articles

Playing with State-Based Models for Designing Better Algorithms

Dominique Méry 1, 2, 3
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : 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.
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Saturday, May 14, 2016 - 8:11:43 AM
Last modification on : Thursday, January 20, 2022 - 5:26:08 PM




Dominique Méry. Playing with State-Based Models for Designing Better Algorithms. Future Generation Computer Systems, Elsevier, 2017, 68, pp.445-455. ⟨10.1016/j.future.2016.04.019⟩. ⟨hal-01316026⟩



Les métriques sont temporairement indisponibles