%0 Conference Paper %1 xu_modelChecking_2009 %A Xu, Dong %A Miao, Huaikou %A Philbert, N. %B Computer and Information Science, 2009. ICIS 2009. Eighth IEEE/ACIS International Conference on %D 2009 %K 2.0 AD CSPM Language;behavior Language;communicating Modeling about activity analysis; analysis;model behavior checking;object-oriented communicating diagnostics;programming diagram;UML industrial language machine;Unified machines;formal model model-checker;Hoare modeling;operational process;UML processes;finite programming;program programs;software reasoning;UML semantics;de-facto semantics;formal semantics;reasoning semantics;software sequential software specification;FDR specification;UML specification;object-oriented standard;formal state system tool;Unified tools;systems verification;UML %P 1035 -1040 %R 10.1109/ICIS.2009.107 %T Model Checking UML Activity Diagrams in FDR %X The Unified Modeling Language (UML) is the de-facto industrial standard for modeling object-oriented software systems. UML activity diagrams (ADs) can be used for software modeling and they have under gone significant changes with UML 2.0 specification, and no longer been a special kind of diagrams of UML state machines. ADs, however, are lack of formal semantics like other diagrams in UML official specifications and therefore they cannot be performed formal system behavior analysis. Verify if a UML model meets the required properties by model checking has become a key issue. Many attempts have been made to provide formalization for UML state diagrams, but little for ADs. This paper formalize the UML ADs and then employs the Hoarepsilas communicating sequential processes to specify its operational and behavior semantics. The presented formalization makes it possible to reason about the behavior of a UML AD in CSP. A software tool for supporting to transfer an AD into CSPM specification has been implemented. Hence it provides an approach to model checking UML ADs by model-checker FDR. Finally, the formalisms and model checking are explicitly illustrated through a simple but non-trivial example.

@inproceedings{xu_modelChecking_2009, abstract = {The Unified Modeling Language (UML) is the de-facto industrial standard for modeling object-oriented software systems. UML activity diagrams (ADs) can be used for software modeling and they have under gone significant changes with UML 2.0 specification, and no longer been a special kind of diagrams of UML state machines. ADs, however, are lack of formal semantics like other diagrams in UML official specifications and therefore they cannot be performed formal system behavior analysis. Verify if a UML model meets the required properties by model checking has become a key issue. Many attempts have been made to provide formalization for UML state diagrams, but little for ADs. This paper formalize the UML ADs and then employs the Hoarepsilas communicating sequential processes to specify its operational and behavior semantics. The presented formalization makes it possible to reason about the behavior of a UML AD in CSP. A software tool for supporting to transfer an AD into CSPM specification has been implemented. Hence it provides an approach to model checking UML ADs by model-checker FDR. Finally, the formalisms and model checking are explicitly illustrated through a simple but non-trivial example.}, added-at = {2013-02-28T11:13:35.000+0100}, author = {Xu, Dong and Miao, Huaikou and Philbert, N.}, biburl = {https://www.bibsonomy.org/bibtex/2d0612cd754d2279a5f331a84aee2147f/fritzsolms}, booktitle = {Computer and Information Science, 2009. ICIS 2009. Eighth IEEE/ACIS International Conference on}, doi = {10.1109/ICIS.2009.107}, interhash = {40041c0da7061c6e11ef144a871a9ed2}, intrahash = {d0612cd754d2279a5f331a84aee2147f}, keywords = {2.0 AD CSPM Language;behavior Language;communicating Modeling about activity analysis; analysis;model behavior checking;object-oriented communicating diagnostics;programming diagram;UML industrial language machine;Unified machines;formal model model-checker;Hoare modeling;operational process;UML processes;finite programming;program programs;software reasoning;UML semantics;de-facto semantics;formal semantics;reasoning semantics;software sequential software specification;FDR specification;UML specification;object-oriented standard;formal state system tool;Unified tools;systems verification;UML}, month = {june}, pages = {1035 -1040}, timestamp = {2013-02-28T11:14:15.000+0100}, title = {Model Checking UML Activity Diagrams in FDR}, year = 2009 }