Publication:4301167

zbMath0855.68060MaRDI QIDQ4301167

Jim Davies, J. C. P. Woodcock

Publication date: 13 July 1994

zbMATH Keywords

refinement calculus; data refinement; specification language \(Z\)

Mathematics Subject Classification ID

68-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Compositionality: Ontology and Mereology of Domains, Extended Static Checking by Calculation Using the Pointfree Transform, Refinement and state machine abstraction, Type inference for set theory, Mechanised support for sound refinement tactics, Experiments in program verification using Event-B, Model evolution and refinement, Mechanical reasoning about families of UTP theories, JCML: A specification language for the runtime verification of Java card programs, Refinement-oriented models of Stateflow charts, On the purpose of Event-B proof obligations, Completeness of fair ASM refinement, A tactic language for refinement of state-rich concurrent specifications, Formalisations and applications of BPMN, ASM refinement and generalizations of forward simulation in data refinement: a comparison, Incompleteness of relational simulations in the blocking paradigm, From control law diagrams to Ada via \textsf{Circus}, Testing for refinement in \textsf{Circus}, Correct hardware synthesis, Verifying data refinements using a model checker, An analysis of refinement in an abortive paradigm, Data refinement and singleton failures refinement are not equivalent, A process algebraic framework for specification and validation of real-time systems, Refinement and verification in component-based model-driven design, Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository, POSIX file store in Z/Eves: An experiment in the verified software repository, A UTP semantics for \textsf{Circus}, Relational concurrent refinement. II: Internal operations and outputs, FDR explorer, A formal framework for modeling and validating simulink diagrams, A calculus for schemas in Z, Abstract state machines: a unifying view of models of computation and of system design frameworks, Efficient symbolic computation of process expressions, Semantics, calculi, and analysis for object-oriented specifications, Composition mechanisms for retrenchment, On the semantics of unified modeling language diagrams using Z notation, Lazy Relations, On the Purpose of Event-B Proof Obligations, A Practical Single Refinement Method for B, Modelling Divergence in Relational Concurrent Refinement

Uses Software

• Z