Home // FUTURE COMPUTING 2015, The Seventh International Conference on Future Computational Technologies and Applications // View article

Specification and Verification of Garbage Collector by Java Modeling Language

Authors:
Wenhui Sun
Yuting Sun
Zhifei Zhang
Jingpeng Tang
Kendall Nygard
Damian Lampl

Keywords: design by contract, Java Modeling Language, garbage collector

Abstract:
The Java garbage collector effectively avoids some security holes and improves the utilization rate of resources. Guaranteed reliability of the garbage collector is a challenge due to the complexity of the interaction between the collector and the user program; the highly abstracted garbage collector algorithms cannot reflect the real implementation details. System complexities have allowed dynamic analysis based on Design by Contract (DBC) to become an important method for ensuring software quality. Java Modeling Language (JML) inherits all the advantages of contractual design, and became a behavior interface specification language for Java. JML can be used to regulate module behavior and detailed design of Java programs. In this paper, we discuss the JML specifications for the functional requirements of the garbage collector in Hoare-style. This approach can improve the reliability and correctness of the software system in the extent of real environments and run-time

Pages: 18 to 23

Copyright: Copyright (c) IARIA, 2015

Publication date: March 22, 2015

Published in: conference

ISSN: 2308-3735

ISBN: 978-1-61208-389-6

Location: Nice, France

Dates: from March 22, 2015 to March 27, 2015