Refinement and reachability in Event\_B

DOI10.1007/11415787_14MaRDI QIDQ5703804zbMATH OpenFDO

Authors Dominique Cansell, Dominique Mery, Jean-Raymond Abrial

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11415787_14

zbMATH Keywords

B MethodReachabilityRefinementStuttering

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The behavioural semantics of Event-B refinement
• Introducing extra operations in refinement
• Foundations for using linear temporal logic in Event-B refinement
• External and internal choice with event groups in Event-B
• Changing system interfaces consistently: a new refinement strategy for CSP\(\|\)B

Cited in

(22)

• External and internal choice with event groups in Event-B
• Validation of formal models by refinement animation
• Verification of compliance for multilevel models in individual trace semantics
• Spot the difference: a detailed comparison between B and Event-B
• Event-B refinement for continuous behaviours approximation
• Reachability analysis and simulation for hybridised Event-B models
• Consistency-preserving refactoring of refinement structures in Event-B models
• Event domains, stable functions and proof-nets
• Generic tools via general refinement
• Relational concurrent refinement: automata
• Proving Quicksort Correct in Event-B
• Foundations for using linear temporal logic in Event-B refinement
• Towards Modelling Obligations in Event-B
• The Composition of Event-B Models
• Experiments in program verification using Event-B
• On the purpose of Event-B proof obligations
• Retrenchment for Event-B: UseCase-wise development and Rodin integration
• More relational concurrent refinement: traces and partial relations
• General refinement. I: Interfaces, determinism and special refinement
• Sound and relaxed behavioural inheritance
• The behavioural semantics of Event-B refinement
• Introducing extra operations in refinement

This page was built for publication: Refinement and reachability in Event\_B

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5703804)