Consistency-preserving refactoring of refinement structures in Event-B models

DOI10.1007/s00165-019-00478-zzbMath1425.68075OpenAlexW2911892608MaRDI QIDQ2418044

Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden

Publication date: 3 June 2019

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

Full work available at URL: https://doi.org/10.1007/s00165-019-00478-z

zbMATH Keywords

interpolationrefinementabstractionEvent-Brefactoringaction systems

Mathematics Subject Classification ID

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

Uses Software

• z3
• Rodin
• ProB

Cites Work

• The ASM refinement method
• Integrating stochastic reasoning into Event-B development
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• The B-Book
• Refinement Calculus
• Abstract State Machines
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item