A UTP semantics for \textsf{Circus}

DOI10.1007/s00165-007-0052-5zbMath1165.68048MaRDI 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 proving; refinement calculus; concurrency; relational model

Mathematics Subject Classification ID

68Q55: Semantics in the theory of computing

68Q65: Abstract data types; algebraic specification

Related Items

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

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