On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems

Abstract : All software systems execute within an environment or context. Reasoning about the correct behavior of such systems is a ternary relation linking the requirements, system and context models. Formal methods are concerned with providing tool (automated) support for the synthesis and analysis of such models. These methods have quite successfully focused on binary relationships, for example: validation of a formal model against an informal one, verification of one formal model against another formal model, generation of code from a design, and generation of tests from requirements. The contexts of the systems in these cases are treated as second-class citizens: in general, the modelling is implicit and usually distributed between the requirements model and the system model. This paper is concerned with the explicit modelling of contexts as first-class citizens and illustrates concepts related to implicit and explicit semantics on an example using the Event B language.
Type de document :
Communication dans un congrès
Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium,, Oct 2014, Corfu, Greece. Springer, 8803, pp.604-618, 2014, Lectures Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-45231-8_50〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01097624
Contributeur : Dominique Méry <>
Soumis le : samedi 20 décembre 2014 - 11:52:56
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Identifiants

  • HAL Id : hal-01097624, version 1

Citation

Yamine Aït Ameur, J. Paul Gibson, Dominique Méry. On Implicit and Explicit Semantics: Integration Issues in Proof-Based Development of Systems. Tiziana Margaria and Bernhard Steffen. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications - 6th International Symposium,, Oct 2014, Corfu, Greece. Springer, 8803, pp.604-618, 2014, Lectures Notes in Computer Science. 〈http://link.springer.com/chapter/10.1007%2F978-3-662-45231-8_50〉. 〈hal-01097624〉

Partager

Métriques

Consultations de la notice

237