Skip to main navigation Skip to search Skip to main content

On implicit and explicit semantics: Integration issues in proof-based development of systems: Version to read

  • Universite Paul Sabatier
  • IT-SudParis
  • Nancy Université

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation - SpecializedTechniques andApplications - 6th International Symposium, ISoLA 2014, Proceedings
EditorsTiziana Margaria, Tiziana Margaria, Bernhard Steffen
PublisherSpringer Verlag
Pages604-618
Number of pages15
ISBN (Electronic)9783662452301
DOIs
Publication statusPublished - 1 Jan 2014
Externally publishedYes
Event6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2014 - Imperial, Corfu, Greece
Duration: 8 Oct 201411 Oct 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8803
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2014
Country/TerritoryGreece
CityImperial, Corfu
Period8/10/1411/10/14

Keywords

  • Contexts
  • Domains
  • Modelling
  • Verification

Fingerprint

Dive into the research topics of 'On implicit and explicit semantics: Integration issues in proof-based development of systems: Version to read'. Together they form a unique fingerprint.

Cite this