Collective Specification and Verification of Behavioral Models and Object-Oriented Implementations
The authors 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, they 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. The experiments show that their performance is similarly comparable to that of manually written programs.