Publication at Faculty of Mathematics and Physics |
2012
Abstract
An important correctness aspect of software built in a modular way is behavior specication 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 be-tween 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.