• Radosław Klimek AGH University of Science and Technology
  • Piotr Szwed AGH University of Science and Technology



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


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.


Download data is not yet available.


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.




How to Cite

Klimek, R., & Szwed, P. (2013). FORMAL ANALYSIS OF USE CASE DIAGRAMS. Computer Science, 11, 115.