Real-time Java API Specifications for High Coverage Test Generation

Wolfgang Ahrendt, Wojciech Mostowski, Gabriele Paganelli

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    11 Citations (Scopus)

    Abstract

    We present the test case generation method and tool KeY-TestGen in the context of real-time Java applications and libraries. The generated tests feature strong coverage criteria, like the Modified Condition/Decision Criterion, by construction. This is achieved by basing the test generation on formal verification techniques, namely the KeY system for Java source code verification. Moreover, we present formal specifications for the classes and methods in the real-time Java API. These specifications are used for symbolic execution when generating tests for real-time Java applications, and for oracle construction when generating tests for realtime Java library implementations. The latter application exhibited a mismatch between a commercial library implementation and the official RTSJ documentation. Even if there is a rationale behind this particular inconsistency, it demonstrates the effectiveness of our method on production code.
    Original languageEnglish
    Title of host publicationJTRES '12
    Subtitle of host publicationProceedings of the 10th International Workshop on Java Technologies for Real-time and Embedded Systems (JTRES 2012)
    Place of PublicationNew York, NY
    PublisherAssociation for Computing Machinery (ACM)
    Pages145-154
    Number of pages10
    ISBN (Print)978-1-4503-1688-0
    DOIs
    Publication statusPublished - Oct 2012
    Event10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2012 - Copenhagen, Denmark
    Duration: 24 Oct 201226 Oct 2012
    Conference number: 10

    Conference

    Conference10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2012
    Abbreviated titleJTRES
    CountryDenmark
    CityCopenhagen
    Period24/10/1226/10/12

    Fingerprint Dive into the research topics of 'Real-time Java API Specifications for High Coverage Test Generation'. Together they form a unique fingerprint.

    Cite this