Radosław Klimek, Piotr Szwed


Use case diagrams play an important role in modeling with UML. Careful modeling is crucialin obtaining a correct and efficient system architecture. The paper refers to the formalanalysis of the use case diagrams. A formal model of use cases is proposed and its constructionfor typical relationships between use cases is described. Two methods of formal analysis andverification are presented. The first one based on a states’ exploration represents a modelchecking approach. The second one refers to the symbolic reasoning using formal methodsof temporal logic. Simple but representative example of the use case scenario verification isdiscussed.


UML; use case; formal model; verification; model checking; temporal logic; semantic tableau

Full Text:



Back R.-J., Petre L., Porres Paltor I.: Analyzing UML Use Case as Contracts. Proceedings of UML’99, Second International Conference on the Unified Modeling Language. (Lecture Notes in Computer Science, 1723), Springer Verlag 1999, pp. 518-533.

Barnett M., Grieskamp W., Schulte W., Tillmann N., Veanes M.: Validating Use-Cases with the AsmL Test Tool. Proc. of the 3rd International Conference on Quality Software (QSIC’03). IEEE Computer Society 2003.

Barrett S., Sinnig D., Chalin P., Butler G.: Merging of Use Case Models: Semantic Foundations. 3rd International Symposium on Theoretical Aspects of Software Engineering, IEEE Computer Society 2009, pp. 182–189.

Bartsch K., Robey M., Ivins J., Lam C.P.: Consistency Checking between Use Case Scenarios and UML Sequence Diagrams. International Conference on Software Engineering, Innsbruck, 2004. IASTED/ACTA Press 2004.

van Benthem J.: Temporal Logic. [in:] Handbook of Logic in Artificial Intelligence and Logic Programming. vol. 4, Clarendon Press 1993–95, pp. 241–350.

Clarke E. M. Jr., Grumberg O., Peled D. A.: Model Checking. MIT Press 1999.

Cockburn A.: Writing Effective Use Cases. Addison-Wesley 2001.

D’Agostino M., Gabbay D.M., H¨ahnle R., Posegga J. (eds): Handbook of Tableau Methods. Kluwer Academic Publishers 1999.

Emerson E. A.: Temporal and Modal Logic. Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, Elsevier, MIT Press 1990, pp. 995-1072.

Fowler M.: UML Distilled. 3rd Edition. Addison-Wesley 2004.

Hurlbut R.: A survey of approaches for describing and formalizing use-cases. Technical Report 9703, Department of Computer Science, Illinois Institute of Technology 1997.

Jacobson I.: Object-Oriented Development in an Industrial Environment. Proc. of OOPSLA’87, special issue of SIGPLAN Notices. vol. 22, 12, 1987, pp. 183–191.

Klimek R., Skrzynski P., Turek M.: Automatic verification of the model at the requirements analysis phase [in Polish]. 12th National Conference of Software Engineering, Poland, Gdansk, September 27-29, PWNT 2010, pp. 209–216.

K¨osters G., Six H.-W., Winter M.: Validation and Verification of Use Cases and Class Models. 7th International Workshop on Requirements Engineering: Foundations for Software Quality (REFSQ’2001, Proc.), 2001.

Król T.: The simulation of use cases [in Polish]. Master thesis (superviser: R. Klimek). AGH University of Science and Technology 2007.

Pohl K., Haumer P.: Modelling Contextual Information about Scenarios. Proc. of the Third International Workshop on Requirements Engineering: Foundations of Software Quality REFSQ’97, Barcelona, 1997, pp. 187–204.

Reisig W.: Petri Nets – An Introduction. (EATCS Monographs on Theoretical Computer Science, Volume 4). Springer Verlag 1985.

Saeki M., Kaiya H., Hattori S.: Applying a Model Checker to Check Regulatory Compliance of Use Case Models. Proc. of CAiSE Forum 2009.

Shen W., Liu S.: Formalization, Testing and Execution of a Use Case Diagram. ICFEM 2003 International Conference on Formal Engineering Methods, Singapore, 2003. (Lecture Notes in Computer Science, 2885), Springer Verlag 2003, pp. 68–85.

Zhao J., Duan Z.: Verification of Use Case with Petri Nets in Requirement Analysis. Proc. of the International Conference on Computational Science and Its Applications, Springer Verlag 2009, pp. 29–42.



  • There are currently no refbacks.