Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
The Safety-Critical Java Mission Model: A Formal Account
verfasst von : Frank Zeyda, Ana Cavalcanti, Andy Wellings
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Safety-Critical Java (SCJ) is a restriction of the Real-Time Specification for Java to support the development and certification of safety-critical applications. It is the result of an international effort from industry and academia. Here we present the first formalisation of the SCJ execution model, covering missions and event handlers. Our formal language is part of the
Circus
family; at the core, we have Z, CSP, and Morgan’s calculus, but we also use object-oriented and timed constructs from the
OhCircus
and
CircusTime
variants. Our work is a first step in the development of refinement-based reasoning techniques for SCJ.