Refinement, decomposition, and instantiation of discrete models: application to Event-B
From MaRDI portal
Publication:5294155
zbMATH Open1118.68392MaRDI QIDQ5294155FDOQ5294155
Authors: Stefan Hallerstede, Jean-Raymond Abrial 
Publication date: 24 July 2007
Recommendations
Cited In (25)
- Title not available (Why is that?)
- Laws of mission-based programming
- Event-B refinement for continuous behaviours approximation
- On the purpose of Event-B proof obligations
- Relating conflict-free stable transition and event models via redex families
- Spot the difference: a detailed comparison between B and Event-B
- Formal models for consent-based privacy
- Composing model programs for analysis
- Refining privacy-aware data flow diagrams
- Experiments in program verification using Event-B
- Theorem proving graph grammars with attributes and negative application conditions
- Derivation of concurrent programs by stepwise scheduling of Event-B models
- Linking event-B and concurrent object-oriented programs
- Patterns for refinement automation
- Developing topology discovery in Event-B
- Proving Quicksort Correct in Event-B
- Atomic actions, and their refinements to isolated protocols
- Building Specifications in the Event-B Institution
- The Composition of Event-B Models
- Consistency-preserving refactoring of refinement structures in Event-B models
- A formal model for blockchain-based consent management in data sharing
- A parametric rely-guarantee reasoning framework for concurrent reactive systems
- On the Purpose of Event-B Proof Obligations
- Incremental System Modelling in Event-B
- Developing Topology Discovery in Event-B
Uses Software
This page was built for publication: Refinement, decomposition, and instantiation of discrete models: application to Event-B
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5294155)
