Composition mechanisms for retrenchment

DOI10.1016/j.jlap.2007.11.001zbMath1137.68037MaRDI QIDQ2426521

M. Poppleton, C. Jeske, Richard Banach

Publication date: 22 April 2008

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://eprints.soton.ac.uk/266492/1/CompMechsRet_JLogAlgPr08.pdf

zbMATH Keywords

decomposition; composition; refinement; model evolution; retrenchment; requirements engineering

Mathematics Subject Classification ID

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

Related Items

Retrenchment and refinement interworking: the tower theorems, The mechanical generation of fault trees for reactive systems via retrenchment. I. Combinational circuits, The mechanical generation of fault trees for reactive systems via retrenchment. II. Clocked and feedback circuits, Retrenchment for Event-B: UseCase-wise development and Rodin integration, Simple feature engineering via neat default retrenchments, Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application, Stronger compositions for retrenchments

Uses Software

• Z

Cites Work

• The mechanical generation of fault trees for reactive systems via retrenchment. I. Combinational circuits
• The mechanical generation of fault trees for reactive systems via retrenchment. II. Clocked and feedback circuits
• Stronger compositions for retrenchments
• Engineering and theoretical underpinnings of retrenchment
• Data Refinement
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item