More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement

No abstract is available for this paper.

• Publication year

  1998

• Venue

  ZUM

• Publication date

  1998-09-24

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/978-3-540-49676-2_20
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Using Z - specification, refinement, and proof

  1996cited by this paper
• How Firing Conditions Help Inheritance

  1995cited by this paper
• Formaliser - An Interactive Support Tool for Z

  1989cited by this paper
• Data Refinement Refined

  1986cited by this paper

• An Assertional Proof of Red–Black Trees Using Dafny

  2019cites this paper
• Retrenchment and refinement interworking: the tower theorems

  2014cites this paper
• Refinement in Z

  2014cites this paper
• From ODP viewpoint consistency to Integrated Formal Methods

  2013cites this paper
• Translation of Z specifications to executable code: Application to the database domain

  2013cites this paper
• On a New Notion of Partial Refinement

  2013cites this paper
• Deriving a Slicing Algorithm via FermaT Transformations

  2011cites this paper
• Derivation of Z functional input/output refinement proof rules

  2010cites this paper
• The Tokeneer Experiments

  2010cites this paper
• Refining interfaces: the case of the B method

  2009cites this paper
• Abstraction of infinite and communicating CSPZ processes

  2009cites this paper
• Non-Classical Hypercomputation

  2009cites this paper
• Checking Z Data Refinements Using Traces Refinement

  2009cites this paper
• Sharp Retrenchment , Modulated Refinement and Punctured Simulation

  2008cites this paper
• Mechanized support for retrenchment

  2008cites this paper
• Verifying Michael and Scott's Lock-Free Queue Algorithm using Trace Reduction

  2008cites this paper
• Reconciling Retrenchments and Refinements II

  2008cites this paper
• The Mondex Purse : Requirements and Retrenchments

  2008cites this paper
• Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1,1) Forward Refinements

  2007cites this paper
• The certification of the Mondex electronic purse to ITSEC Level E6

  2007cites this paper
• Engineering and theoretical underpinnings of retrenchment

  2007cites this paper
• Mechanising Mondex with Z/Eves

  2007cites this paper
• On using data abstractions for model checking refinements

  2007cites this paper
• Verifying Michael and Scott ’ s Lock-Free Queue Algorithm using Trace Reduction

  2007cites this paper
• Retrenchment , Refinement , and Notions of Simulation

  2007cites this paper
• Ðððòòòòò Óöññð Ëô Blockin Blockin¬ Blockin Blockinøøóò× Ý Åùøøøøóòò Ëè ×× Blockinùööøý Üüñôðð Ìììøøññ Ëööúøøòòòùð £ ¸ Âóóò º Ððöö¸ëù××ò Ëøøôòòý¸òò Óòò Èóðð

  2007cites this paper
• An analysis of refinement in an abortive paradigm

  2006influential citation
• Engineering emergence

  2006cites this paper
• Software Abstractions - Logic, Language, and Analysis

  2006cites this paper
• Action Refinement Applied to Late Decisions

  2006cites this paper
• Algebraic Integration of Retrenchment and Refinement

  2006cites this paper
• Z/Eves and the Mondex Electronic Purse

  2006cites this paper
• Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern

  2005cites this paper
• Breaking the Model: Finalisation and a Taxonomy of Security Attacks

  2005cites this paper
• Retrenchment and the Mondex Electronic Purse

  2005cites this paper
• 2 The Mondex Purse : from Refinement to Retrenchment

  2005cites this paper
• Non-atomic Refinement in Z and CSP

  2005cites this paper
• Pigs from sausages? Reengineering from assembler to C via FermaT transformations

  2004cites this paper
• Using Coupled Simulations in Non-atomic Refinement

  2003cites this paper
• Recent Advances in Refinement

  2003cites this paper
• Introducing Backward Refinement into B

  2003cites this paper
• Challenging formal specifications by mutation: a CSP security example

  2003cites this paper
• Action refinement in end-based choice settings

  2003cites this paper
• Minimally and Maximally Abstract Retrenchments

  2002cites this paper
• Controlling Control Systems: An Application of Evolving Retrenchment

  2002cites this paper
• Checking Z Data Refinements Using an Animation Tool

  2002cites this paper
• Derivation of Z refinement proof rules: Forwards and backwards rules incorporating input/output refi

  2002cites this paper
• Reconciling Retrenchments and Refinements I

  2002cites this paper
• Maude meets CORBA

  2001cites this paper
• A generic proof checker

  2001cites this paper
• From Maude Specifications to SOAP Distributed Implementations: A Smooth Transition

  2001cites this paper
• Liberating Data Refinement

  2000cites this paper
• Segregation with Communication

  2000cites this paper
• Is Proof More Cost-Effective Than Testing?

  2000cites this paper
• Retrenchment: Extending Re(cid:12)nement for Continuous and Control Systems

  2000cites this paper
• Retrenchment: Extending Refinement for Continuous and Control Systems

  2000cites this paper
• Filter promotion transformation strategies for deriving efficient programs from Z specifications

  2000cites this paper
• Retrenchment, Refinement, and Simulation

  2000cites this paper
• Maximally abstract retrenchments

  2000cites this paper
• Viewpoint consistency in ODP

  2000cites this paper
• Formal Methods for Industrial Products

  2000cites this paper
• Systems Development Using Z Generics

  1999cites this paper
• Retrenchment and Punctured Simulation

  1999cites this paper
• A Junction between State Based and Behavioural Specification (Invited Talk)

  1999cites this paper
• Non-atomic Refinement in Z

  1999cites this paper
• The Value of Verification: Positive Experience of Industrial Proof

  1999cites this paper
• Sharp Retrenchment, Modulated Refinement and Simulation

  1999cites this paper
• IO-refinement in Z

  1998cites this paper
• The IFAD VDM Tools: Lightweight Formal Methods

  1998cites this paper