COLLECTIVE SPECIFICATION AND VERIFICATION OF BEHAVIOR MODELS AND OBJECT-ORIENTED IMPLEMENTATIONS

Qing Yi, Jianwei Niu, Anitha R. Marneni

2011

Abstract

We present a finite-state-machine-based language, iFSM, to seamlessly integrate the behavioral logic and implementation strategies of object-oriented abstractions and prevent them from being out-of-sync. We provide a transformation engine which automatically translates iFSM specifications to lower-level C++/Java class implementations that are similar in style to manually written code. Further, we automatically verify that these implementations are consistent with their behavior models by translating iFSM specifications into the input language of model checker NuSMV.

Paper Citation

in Harvard Style

Yi Q., Niu J. and R. Marneni A. (2011). COLLECTIVE SPECIFICATION AND VERIFICATION OF BEHAVIOR MODELS AND OBJECT-ORIENTED IMPLEMENTATIONS . In Proceedings of the 6th International Conference on Software and Database Technologies - Volume 2: ICSOFT, ISBN 978-989-8425-77-5, pages 15-24. DOI: 10.5220/0003439300150024

in Bibtex Style

@conference{icsoft11,
author={Qing Yi and Jianwei Niu and Anitha R. Marneni},
title={COLLECTIVE SPECIFICATION AND VERIFICATION OF BEHAVIOR MODELS AND OBJECT-ORIENTED IMPLEMENTATIONS},
booktitle={Proceedings of the 6th International Conference on Software and Database Technologies - Volume 2: ICSOFT,},
year={2011},
pages={15-24},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0003439300150024},
isbn={978-989-8425-77-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 6th International Conference on Software and Database Technologies - Volume 2: ICSOFT,
TI - COLLECTIVE SPECIFICATION AND VERIFICATION OF BEHAVIOR MODELS AND OBJECT-ORIENTED IMPLEMENTATIONS
SN - 978-989-8425-77-5
AU - Yi Q.
AU - Niu J.
AU - R. Marneni A.
PY - 2011
SP - 15
EP - 24
DO - 10.5220/0003439300150024