Safety-critical Java programs from \textsf{Circus} models

DOI10.1007/S11241-013-9182-4MaRDI QIDQ2443940zbMATH OpenOpenAlexFDO

Authors Ana Cavalcanti, Frank Zeyda, Andy Wellings, Kun Wei, Jim Woodcock

Publication date 8 April 2014

Published in Real-Time Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11241-013-9182-4

zbMATH Keywords

\textsf{Circus}real-time systemsrefinementRTSJSCJverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Laws of mission-based programming
• The safety-critical Java memory model formalised
• Algebraic compilation of safety-critical Java bytecode
• From safety critical Java programs to timed process models
• Specification and runtime verification of Java card programs

Cites work

• A process algebraic framework for specification and validation of real-time systems
• A refinement strategy for Circus
• A sequential real-time refinement calculus
• A Theory of Pointers for the UTP
• A timed model for communicating sequential processes
• A UTP semantics for \textsf{Circus}
• Auxiliary variables in data refinement
• Concurrent and Real-Time Programming in Ada 2005
• From control law diagrams to Ada via \textsf{Circus}
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• Integrated Formal Methods
• Mechanised support for sound refinement tactics
• Object-Orientation in the UTP
• Refinement-oriented models of Stateflow charts
• Region-based memory management
• The Miracle of Reactive Programming
• The safety-critical Java memory model formalised
• Using the Alloy analyzer to verify data refinement in Z
• ZRC -- A refinement calculus for Z

Cited in

(6)

• Compiling and verifying SC-SystemJ programs for safety-critical reactive systems
• The safety-critical Java memory model formalised
• Laws of mission-based programming
• Towards Algebraic Semantics of Circus Time
• From safety critical Java programs to timed process models
• Algebraic compilation of safety-critical Java bytecode

Describes a project that uses

Uses Software

• Circus
• Z
• CirCUs
• ZRC

This page was built for publication: Safety-critical Java programs from \textsf{Circus} models

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