EVALUATING UML SEQUENCE MODELS USING THE SPIN MODEL CHECKER

Yoshiyuki Shinkawa

2010

Abstract

UML sequence diagram is one of the most important diagrams for behavior modeling, however there are few established criteria, methodologies and processes to evaluate the correctness of the models depicted by this diagram. This paper proposes a formal approach to evaluating the correctness of UML sequence models using the SPIN model checker. In order to deal with the models by the SPIN, they must be expressed in the form of Promela codes and LTL formula. A set of definite rules is presented, which can extract the above codes and formulae from given UML sequence models.

Paper Citation

in Harvard Style

Shinkawa Y. (2010). EVALUATING UML SEQUENCE MODELS USING THE SPIN MODEL CHECKER . In Proceedings of the 12th International Conference on Enterprise Information Systems - Volume 3: ICEIS, ISBN 978-989-8425-06-5, pages 417-422. DOI: 10.5220/0002870304170422

in Bibtex Style

@conference{iceis10,
author={Yoshiyuki Shinkawa},
title={EVALUATING UML SEQUENCE MODELS USING THE SPIN MODEL CHECKER},
booktitle={Proceedings of the 12th International Conference on Enterprise Information Systems - Volume 3: ICEIS,},
year={2010},
pages={417-422},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002870304170422},
isbn={978-989-8425-06-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 12th International Conference on Enterprise Information Systems - Volume 3: ICEIS,
TI - EVALUATING UML SEQUENCE MODELS USING THE SPIN MODEL CHECKER
SN - 978-989-8425-06-5
AU - Shinkawa Y.
PY - 2010
SP - 417
EP - 422
DO - 10.5220/0002870304170422