Playing with State-Based Models for Designing Better Algorithms

Dominique Méry 1, 2, 3, 4
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Liste complète des métadonnées

https://hal.inria.fr/hal-01316026
Contributeur : Dominique Méry <>
Soumis le : samedi 14 mai 2016 - 08:11:43
Dernière modification le : mardi 13 décembre 2016 - 15:45:06

Identifiants

  • HAL Id : hal-01316026, version 1

Collections

Citation

Dominique Méry. Playing with State-Based Models for Designing Better Algorithms. Future Generation Computer Systems, Elsevier, 2016, pp.25. 〈ELSEVIER〉. 〈hal-01316026〉

Partager

Métriques

Consultations de la notice

279