The safety-critical Java memory model formalised

DOI10.1007/S00165-012-0253-4MaRDI QIDQ1941888zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Andy Wellings, Jim 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

integrationmemory safetyrefinementsafety-critical Javasemanticsunifying theories of programming

Mathematics Subject Classification ID

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

Recommendations

• Java and the Java memory model -- a unified, machine-checked formalisation
• scientific article; zbMATH DE number 1951189
• Java Memory Model-Aware Model Checking
• Safety-critical Java programs from \textsf{Circus} models
• scientific article; zbMATH DE number 1617288
• The Java Memory Model: Operationally, Denotationally, Axiomatically

Cites work

• A process algebraic framework for specification and validation of real-time systems
• A Theory of Pointers for the UTP
• A UTP semantics for \textsf{Circus}
• Compositional Reasoning for Pointer Structures
• scientific article; zbMATH DE number 1031982 (Why is no real title available?)
• Pointers and Records in the Unifying Theories of Programming
• UTP Semantics for Web Services

Cited in

(18)

• A Ravenscar-compliant run-time kernel for safety-critical systems
• A UTP approach for rTiMo
• A process calculus BigrTiMo of mobile systems and its formal semantics
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• Laws of mission-based programming
• Safety-critical Java programs from \textsf{Circus} models
• scientific article; zbMATH DE number 1617288 (Why is no real title available?)
• Isabelle/UTP: a mechanised theory engineering framework
• Java and the Java memory model -- a unified, machine-checked formalisation
• Java Memory Model-Aware Model Checking
• An Axiomatic Value Model for Isabelle/UTP
• From safety critical Java programs to timed process models
• scientific article; zbMATH DE number 1951189 (Why is no real title available?)
• Algebraic compilation of safety-critical Java bytecode
• The Java Memory Model: Operationally, Denotationally, Axiomatically
• An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency
• Denotational semantics and its algebraic derivation for an event-driven system-level language
• Scoped types and aspects for real-time Java memory management

Describes a project that uses

Uses Software

• Circus
• SafeJML
• SPARK
• JML

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1941888)