The safety-critical Java memory model formalised

DOI10.1007/s00165-012-0253-4zbMath1259.68029OpenAlexW2061414465MaRDI QIDQ1941888

Ana Cavalcanti, Andy Wellings, J. C. P. Woodcock

Publication date: 22 March 2013

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

Full work available at URL: https://doi.org/10.1007/s00165-012-0253-4

zbMATH Keywords

integrationsemanticsrefinementunifying theories of programmingmemory safetysafety-critical Java

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

A UTP approach for rTiMo ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Denotational semantics and its algebraic derivation for an event-driven system-level language ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ Safety-critical Java programs from \textsf{Circus} models ⋮ A process calculus BigrTiMo of mobile systems and its formal semantics ⋮ Isabelle/UTP: A Mechanised Theory Engineering Framework

Uses Software

• SPARK
• JML
• Circus
• SafeJML

Cites Work

• Unnamed Item
• A process algebraic framework for specification and validation of real-time systems
• A UTP semantics for \textsf{Circus}
• UTP Semantics for Web Services
• Compositional Reasoning for Pointer Structures
• Pointers and Records in the Unifying Theories of Programming
• A Theory of Pointers for the UTP

This page was built for publication: The safety-critical Java memory model formalised