Specifying subtypes in Safety Critical Java programs. (4th October 2012)

• Record Type: Journal Article
• Authors: Haddad, Ghaith; Leavens, Gary T.
• Other Names: Ravn Anders P. guestEditor.; Higuera‐Toledano M. Teresa guestEditor.; Porto Fabio guestEditor.; Schulze Bruno guestEditor.
• Is Part Of: Concurrency and computation. Volume 25:Number 16(2013:Nov.)
• Page Start: 2290
• Page End: 2306
• Publication Date: 2012-10-04
• Subjects: SafeJML -- Safety Critical Java (SCJ) -- Java Modeling Language (JML) -- timing behavior -- duration -- performance -- WCET; Parallel processing (Electronic computers) -- Periodicals; Parallel computers -- Periodicals; 004.35
• DOI: 10.1002/cpe.2930
• Languages: English
• ISSNs: 1532-0626

Abstract

SUMMARY: 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 methodscale is specified in a supertypeVector2d to take at most 42 ns to execute, then an override ofscale cannot take more than 42 ns to execute in any subtype, such asVector3d . The problem is that subtype objects typically contain more information, such as thez coordinate inVector3d, 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 © 2012 John Wiley & Sons, Ltd.