Compositional verification for Object-Z

DOI10.1007/3-540-44880-2_18MaRDI QIDQ4436973zbMATH OpenFDO

Authors Kirsten Winter, Graeme Smith

Publication date 4 December 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2651/26510280.htm

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 860045
• Specification, refinement and verification of concurrent systems -- an integration of Object-\(Z\) and \(CSP\)
• Structuring real-time Object-Z specifications
• Compositional verification in linear-time temporal logic
• Proving temporal properties of Z specifications using abstraction

Cited in

(7)

• Constructive consistency checking for partial specification in Z
• Slicing techniques for verification re-use
• A basic calculus for verifying properties of interacting objects
• A compositional trace logic for behavioural interface specifications
• Decomposing Integrated Specifications for Verification
• Proving temporal properties of Z specifications using abstraction
• FM 2005: Formal Methods

This page was built for publication: Compositional verification for Object-Z

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