Laws of mission-based programming

DOI10.1007/S00165-014-0317-8MaRDI QIDQ2355382zbMATH OpenOpenAlexFDO

Authors Frank Zeyda, Ana Cavalcanti

Publication date 23 July 2015

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

Full work available at URL https://research.tees.ac.uk/en/publications/945d7b9e-e65a-493d-a5be-176ab3e9d3f8

zbMATH Keywords

automationCircuslawsmodelspatternsproofrefinementSCJ

Mathematics Subject Classification ID

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

Recommendations

• Safety-critical Java programs from \textsf{Circus} models
• 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 tactic language for refinement of state-rich concurrent specifications
• A timed model for communicating sequential processes
• A UTP semantics for \textsf{Circus}
• Complete integer decision procedures as derived rules in HOL
• Compositional action system refinement
• CSP theorems for communicating B machines
• 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?)
• Mechanised support for sound refinement tactics
• Modeling in Event B. System and software engineering.
• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• Safety-critical Java programs from \textsf{Circus} models
• ZRC -- A refinement calculus for Z

Cited in

(4)

• Safety-critical Java programs from \textsf{Circus} models
• From safety critical Java programs to timed process models
• Algebraic compilation of safety-critical Java bytecode
• Lawful functions and program verification in miranda

Describes a project that uses

Uses Software

• CirCUs
• ZRC
• Z
• ArcAngelC
• Circus

This page was built for publication: Laws of mission-based programming

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