BeJC: Checking Compliance Between Java Implementation and Behavior Specification

Abstract:

An important correctness aspect of software built in a modular way is behavior specification of its particular components. Only then one can reason about communication correctness and properties of particular components. Since it is much more effective to do so at the level of behavior models, establishing a correspondence between behavior specification and implementation becomes an important part. In this paper, we present a method for verifying compliance between behavior specification of a software component and its Java implementation. We also discuss practical experience with the BeJC tool that implements the compliance checking algorithm and its application in the software development process.

BibTeX:

@inproceedings{jancik_bejc_2012,
    title = {{BeJC: Checking Compliance Between Java Implementation and Behavior Specification}},
    author = {Janč ík, Pavel and Parízek, Pavel and Kofroň, Jan},
    year = {2012},
    booktitle = {{Proceedings of WCOP 2014}},
    publisher = {ACM},
    series = {{WCOP '12}},
    location = {New York, NY, USA},
    doi = {10.1145/2304676.2304683},
    isbn = {978-1-4503-1348-3},
    pages = {31--36},
    url = {http://doi.acm.org/10.1145/2304676.2304683},
    shorttitle = {BeJC},
}

Proceedings paper