Patterns for refinement automation

DOI10.1007/978-3-642-17071-3_4MaRDI QIDQ3066119zbMATH OpenOpenAlexFDO

Authors Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky

Publication date 8 January 2011

Published in Formal Methods for Components and Objects (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-17071-3_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of software (68N99)

Recommendations

• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• Refinement patterns for ASTDs
• Pattern-based rewriting through abstraction
• Towards software design automation with patterns
• scientific article; zbMATH DE number 2033524

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 1006119 (Why is no real title available?)
• scientific article; zbMATH DE number 1104377 (Why is no real title available?)
• An axiomatic basis for computer programming
• ArcAngel: a tactic language for refinement
• Refinement Calculus
• Superposition refinement of reactive systems
• The B-Book
• The Use of Triple-Modular Redundancy to Improve Computer Reliability

Cited in

(10)

• Mechanised support for sound refinement tactics
• Pattern-based rewriting through abstraction
• scientific article; zbMATH DE number 2033524 (Why is no real title available?)
• Towards software design automation with patterns
• Refinement patterns for ASTDs
• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• Refining emergent properties
• Formalization of invariant patterns for the invariant refinement method
• Automating Event-B invariant proofs by rippling and proof patching
• Validation of formal models by refinement animation

Describes a project that uses

Uses Software

• ArcAngel

This page was built for publication: Patterns for refinement automation

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