Collective Specification and Verification of Behavioral Models and Object-oriented Implementations

We present a finite-state-machine-based language, iFSM, to seamlessly integrate the behavioral logic and implementation strategies of object-oriented applications to prevent their design and implementation from being out-of-sync. The language allows developers to focus on higher-level abstractions to support software analysis and design instead of focusing on language or architecture specific details. To support the language, we provide a transformation engine which automatically translates iFSM specifications to lower-level C++/Java implementations of object-oriented classes. The auto-generated implementations from iFSM are similar in style to the manually written code, so that they are readable and easily integrable with the existing code. Our experiments show that their performance is similarly comparable to that of manually written programs. We have automatically verified that these implementations are consistent with their behavioral models by translating iFSM specifications into the input language of model checker NuSMV.