Private memory allocation analysis for safety-critical java

Andreas Engelbredt Dalsgaard, Rene Rydhof Hansen, Martin Schoeberl

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

7 Citations (Scopus)

Abstract

Safety-critical Java (SCJ) avoids garbage collection and uses a scope based memory model. This memory model is based on a restricted version of RTSJ [2] style scopes. The scopes form a clear hierarchy with different lifetimes. Therefore, references between objects in different scopes are only al- lowed from objects allocated in scopes with a shorter lifetime to objects allocated in scopes with a longer lifetime. To ensure memory safety, programmers are required to either manually annotate the application with complex annotations, rely on a runtime test of each reference assignment, or statically analyze all reference assignments and avoid run- time checks when all assignments are proven to be correct. A violation of the assignment rule at runtime leads to an unchecked exception. For safety-critical code that needs to be certified, runtime exceptions must be avoided and the absence of illegal reference assignments needs to be proven. In this paper we present a static program analysis tool that automates the proof that no illegal assignments occur.
Original languageEnglish
Title of host publicationJTRES '12 Proceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems
Number of pages9
PublisherAssociation for Computing Machinery
Publication date2012
Pages9-17
ISBN (Print)978-1-4503-1688-0
DOIs
Publication statusPublished - 2012
SeriesProceedings of the International Workshop of Java Technologies for Real-Time and Embedded Systems
ISSN2154-056X

Fingerprint

Dive into the research topics of 'Private memory allocation analysis for safety-critical java'. Together they form a unique fingerprint.

Cite this