Retrenchment for Event-B: UseCase-wise development and Rodin integration

DOI10.1007/S00165-009-0139-2MaRDI QIDQ539231zbMATH OpenOpenAlexFDO

Authors Richard Banach

Publication date 27 May 2011

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

Full work available at URL https://doi.org/10.1007/s00165-009-0139-2

zbMATH Keywords

refinementEvent-Bretrenchmentincremental developmentRodin toolsettower patternUseCase-wise development

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Engineering and theoretical underpinnings of retrenchment
• Retrenchment and refinement interworking: the tower theorems
• scientific article; zbMATH DE number 1487747
• Composition mechanisms for retrenchment
• The behavioural semantics of Event-B refinement

Cites work

• scientific article; zbMATH DE number 2227867 (Why is no real title available?)
• Composition mechanisms for retrenchment
• Engineering and theoretical underpinnings of retrenchment
• FM 2005: Formal Methods
• On regularity in software design
• Retrenching the purse: the balance enquiry quandary, and generalised and \((1, 1)\) forward refinements
• Retrenchment and refinement interworking: the tower theorems
• Superposition refinement of reactive systems
• The B-Book

Cited in

(1)

• Retrenchment and refinement interworking: the tower theorems

Describes a project that uses

Uses Software

• Rodin

This page was built for publication: Retrenchment for Event-B: UseCase-wise development and Rodin integration

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