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

DOI10.1007/S00165-009-0139-2zbMATH Open1214.68129OpenAlexW2138824635MaRDI QIDQ539231FDOQ539231

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

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

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)

Cites Work

• The B-Book
• Engineering and theoretical underpinnings of retrenchment
• Superposition refinement of reactive systems
• Title not available (Why is that?)
• Composition mechanisms for retrenchment
• FM 2005: Formal Methods
• Retrenchment and refinement interworking: the tower theorems
• On regularity in software design
• Retrenching the purse: the balance enquiry quandary, and generalised and \((1, 1)\) forward refinements

Cited In (1)

• Retrenchment and refinement interworking: the tower theorems

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)