Safety-critical Java programs from Circus models

TY - JOUR

T1 - Safety-critical Java programs from Circus models

AU - Cavalcanti, Ana Lucia Caneca

AU - Zeyda, Frank

AU - Wellings, Andy

AU - Woodcock, Jim

AU - Wei, Kun

PY - 2013/9

Y1 - 2013/9

N2 - Safety-Critical Java (SCJ) is a novel version of Java that addresses issues related to real-time programming and certification of safety-critical applications. In this paper, we propose a technique that reveals the issues involved in the formal verification of an SCJ program, and provides guidelines for tackling them in a refinement-based approach. It is based on Circus, a combination of well established notations: Z, CSP, Timed CSP, and object orientation. We cater for the specification of timing requirements and their decomposition towards the structure of missions and event handlers of SCJ. We also consider the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. We present a refinement strategy, a Circus variant that captures the essence of the SCJ paradigm, and a substantial example based approach on a concurrent version of a case study that has been used as a benchmark by the SCJ community: an aircraft collision detector.

AB - Safety-Critical Java (SCJ) is a novel version of Java that addresses issues related to real-time programming and certification of safety-critical applications. In this paper, we propose a technique that reveals the issues involved in the formal verification of an SCJ program, and provides guidelines for tackling them in a refinement-based approach. It is based on Circus, a combination of well established notations: Z, CSP, Timed CSP, and object orientation. We cater for the specification of timing requirements and their decomposition towards the structure of missions and event handlers of SCJ. We also consider the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. We present a refinement strategy, a Circus variant that captures the essence of the SCJ paradigm, and a substantial example based approach on a concurrent version of a case study that has been used as a benchmark by the SCJ community: an aircraft collision detector.

KW - SCJ

KW - Circus

KW - RTSJ

KW - Real-time systems

KW - Refinement

KW - Verification

U2 - 10.1007/s11241-013-9182-4

DO - 10.1007/s11241-013-9182-4

M3 - Article

SN - 0922-6443

VL - 49

SP - 614

EP - 667

JO - Real-Time Systems

JF - Real-Time Systems

IS - 5

ER -