The behavioural semantics of Event-B refinement

DOI10.1007/s00165-012-0265-0zbMath1342.68211OpenAlexW2001570688WikidataQ60173560 ScholiaQ60173560MaRDI QIDQ736910

Helen Treharne, Heike Wehrheim, S. A. Schneider

Publication date: 5 August 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: http://epubs.surrey.ac.uk/726036/4/facs-refine11.pdf

zbMATH Keywords

CSPrefinementtracesEvent-Bdevelopment strategydivergences

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Building Specifications in the Event-B Institution, Foundations for using linear temporal logic in Event-B refinement, The behavioural semantics of Event-B refinement, Static and dynamic property-preserving updates, Static Livelock Analysis in CSP

Uses Software

• Alloy
• Rodin
• csp2B
• Z
• FDR2
• Circus

Cites Work

• On the purpose of Event-B proof obligations
• Structural refinement of systems specified in Object-Z and CSP
• Relational concurrent refinement
• The behavioural semantics of Event-B refinement
• Specification and (property) inheritance in CSP-OZ
• External and internal choice with event groups in Event-B
• CSP theorems for communicating B machines
• Modelling Divergence in Relational Concurrent Refinement
• The B-Book
• Refinement Calculus
• The specification statement
• csp2B: A practical approach to combining CSP and B
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item