A tactic language for refinement of state-rich concurrent specifications

DOI10.1016/j.scico.2010.11.012zbMath1218.68101OpenAlexW2033328719MaRDI QIDQ541214

Ana Cavalcanti, Frank Zeyda, Marcel V. M. Oliveira

Publication date: 6 June 2011

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2010.11.012

zbMATH Keywords

refinement calculusconcurrencycontrol law diagramstactics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Mechanised support for sound refinement tactics ⋮ Automating Refinement of Circus Programs ⋮ ArcAngelC ⋮ Laws of mission-based programming

Uses Software

• Matlab
• ArcAngel
• ProofPower
• ClawZ
• Z/EVES
• Z
• ZRC
• Circus
• Cambridge LCF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ArcAngel: a tactic language for refinement
• A refinement strategy for Circus
• Data refinement by calculation
• Refinement concepts formalised in higher order logic
• A UTP semantics for \textsf{Circus}
• A program refinement tool
• ZRC -- A refinement calculus for \(Z\)
• Mechanizing some advanced refinement concepts
• Edinburgh LCF. A mechanized logic of computation
• A tactic calculus. --- Abridged version
• A Guide to MATLAB
• PVS#: Streamlined Tacticals for PVS
• Type Checking Specifications
• Logic and Computation
• FM 2005: Formal Methods

This page was built for publication: A tactic language for refinement of state-rich concurrent specifications