Checking Z Data Refinements Using Traces Refinement

DOI10.1016/J.ENTCS.2009.05.049MaRDI QIDQ5179359zbMATH OpenOpenAlexFDO

Authors André Didier, Adalberto Farias, Alexandre Mota

Publication date 19 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.05.049

zbMATH Keywords

data refinementmodel checkingZ

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 2079995
• Using the Alloy analyzer to verify data refinement in Z
• ZB 2005: Formal Specification and Development in Z and B
• Verifying data refinements using a model checker
• scientific article; zbMATH DE number 4026807
• Refinement of Trace Abstraction
• Test selection for traces refinement
• scientific article; zbMATH DE number 1569130
• scientific article; zbMATH DE number 1615985
• Some proofs of data refinement

Cites work

• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 2013587 (Why is no real title available?)
• scientific article; zbMATH DE number 1487738 (Why is no real title available?)
• scientific article; zbMATH DE number 2090136 (Why is no real title available?)
• Integrated Formal Methods
• Model-checking CSP-Z: Strategy, tool support and industrial application
• On using data abstractions for model checking refinements
• Proof theory and automated deduction
• Using the Alloy analyzer to verify data refinement in Z
• Verifying data refinements using a model checker

Cited in

(6)

• Refinement for user interface designs
• scientific article; zbMATH DE number 1612491 (Why is no real title available?)
• Using the Alloy analyzer to verify data refinement in Z
• scientific article; zbMATH DE number 2079995 (Why is no real title available?)
• Theorem Proving in Higher Order Logics
• A formal software development approach using refinement calculus

Describes a project that uses

Uses Software

• Z

This page was built for publication: Checking Z Data Refinements Using Traces Refinement

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