A UTP semantics for \textsf{Circus}

DOI10.1007/s00165-007-0052-5zbMath1165.68048OpenAlexW1976054113MaRDI QIDQ1019016

Ana Cavalcanti, J. C. P. Woodcock, Marcel V. M. Oliveira

Publication date: 27 May 2009

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-007-0052-5

zbMATH Keywords

theorem provingrefinement calculusconcurrencyrelational model

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65)

Related Items (35)

Circus Time with Reactive Designs ⋮ The Logic of U ·(TP)2 ⋮ Behavioural Models for FMI Co-simulations ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Building Specifications in the Event-B Institution ⋮ Reasoning about iteration and recursion uniformly based on big-step semantics ⋮ Unifying Theories of Programming in Isabelle ⋮ Information Flow Control-by-Construction for an Object-Oriented Language ⋮ Flexible Correct-by-Construction Programming ⋮ The safety-critical Java memory model formalised ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Categorical foundations for structured specifications in \(\mathsf{Z}\) ⋮ Denotational semantics and its algebraic derivation for an event-driven system-level language ⋮ Mechanised support for sound refinement tactics ⋮ Mechanical reasoning about families of UTP theories ⋮ A Stepwise Approach to Linking Theories ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ From control law diagrams to Ada via \textsf{Circus} ⋮ Unifying theories of time with generalised reactive processes ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ Test selection for traces refinement ⋮ RiskStructures: a design algebra for risk-aware machines ⋮ Modelling temporal behaviour in complex systems with Timebands ⋮ A tactic language for refinement of state-rich concurrent specifications ⋮ Unifying theories of reactive design contracts ⋮ Model transformations across views ⋮ A timeband framework for modelling real-time systems ⋮ A UTP semantics for communicating processes with shared variables and its formal encoding in PVS ⋮ On integrating confidentiality and functionality in a formal method ⋮ Automated verification of reactive and concurrent programs by calculation ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework ⋮ Towards Algebraic Semantics of Circus Time ⋮ Testing for refinement in \textsf{Circus} ⋮ Simulink Timed Models for Program Verification ⋮ Laws of mission-based programming

Uses Software

• ProofPower
• Z/EVES
• Z
• ZRC
• Circus

Cites Work

• A theoretical basis for stepwise refinement and the programming calculus
• A refinement strategy for Circus
• ZRC -- A refinement calculus for \(Z\)
• Unifying Theories in ProofPower-Z
• Mechanising a Unifying Theory
• FM 2005: Formal Methods
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A UTP semantics for \textsf{Circus}