Specifying subtypes in Safety Critical Java programs

    Authors

    G. Haddad;G. T. Leavens

    Comments

    Authors: contact us about adding a copy of your work at STARS@ucf.edu

    Abbreviated Journal Title

    Concurr. Comput.-Pract. Exp.

    Keywords

    SafeJML; Safety Critical Java (SCJ); Java Modeling Language (JML); timing behavior; duration; performance; WCET; SPECIFICATION; VERIFICATION; ABSTRACTION; Computer Science, Software Engineering; Computer Science, Theory &; Methods

    Abstract

    Real-time and safety-critical code could benefit from the use of design patterns and frameworks that rely on subtyping and dynamic dispatch. However, modular reasoning about programs that use subtypes requires that each overriding method obeys the specifications of all methods that it overrides. For example, if method scale is specified in a supertype Vector2d to take at most 42ns to execute, then an override of scale cannot take more than 42ns to execute in any subtype, such as Vector3d. The problem is that subtype objects typically contain more information, such as the z coordinate in Vector3d, and thus their methods often require more time to execute than the methods they override. In this paper, we show how to specify timing constraints for subtypes in a way that both allows overriding subtype methods to have more time to execute and yet permits precise modular verification and checking of timing constraints. Our techniques allow object-oriented coding and design patterns based on subtype polymorphism to be used in real-time and safety-critical software. Copyright (c) 2012 John Wiley & Sons, Ltd.

    Journal Title

    Concurrency and Computation-Practice & Experience

    Volume

    25

    Issue/Number

    16

    Publication Date

    1-1-2013

    Document Type

    Article

    Language

    English

    First Page

    2290

    Last Page

    2306

    WOS Identifier

    WOS:000326023300005

    ISSN

    1532-0626

    Share

    COinS