Safety-critical Java in Circus
Ana Cavalcanti, Andy J. Wellings, Jim Woodcock, Kun Wei, Frank Zeyda · 2011
This position paper proposes a refinement technique for the development of Safety-Critical Java (SCJ) programs. It is based on the Circus family of languages, which comprises constructs from 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, and a Circus variant that captures the essence of the SCJ paradigm independently from Java.