Formal analysis of use case diagrams

• Autorzy: Klimek R. , Szwed P.

Warianty tytułu

PL

Formalna analiza diagramów przypadków użycia

• Języki publikacji: EN

Abstrakty

EN

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

PL

Diagramy przypadków użycia odgrywają znaczącą rolę w modelowaniu systemów z wykorzystaniem UML. Staranne i dokładne modelowanie ma zasadnicze znaczenie w postępowaniu umożliwiającym uzyskanie poprawnej i efektywnej architektury systemu. Artykuł odnosi się do formalnej analizy diagramów przypadków użycia. Został zaproponowany model formalny przypadku użycia, a także opisano odpowiednie konstrukcje dla relacji występujących pomiędzy przypadkami użycia. Zostały przedstawione dwie formalne metody ich analizy i weryfikacji. Pierwsza oparta jest na eksploracji stanów i reprezentuje podejście nazwane weryfikacją modelową. Druga odwołuje się do wnioskowania symbolicznego z wykorzystaniem logiki temporalnej. Został pokazany prosty i reprezentatywny przykład weryfikacji pewnego scenariusza przypadku użycia.

Słowa kluczowe

EN

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

PL

UML; przypadek użycia; model formalny; weryfikacja; weryfikacja modelowa; logika temporalna; metoda tablic semantycznych

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2010
• Tom: Vol. 11
• Strony: 115--131
• Opis fizyczny: Bibliogr. 20 poz., rys., tab.

Twórcy

autor

Klimek R.

• AGH University of Science and Technology, al. Mickiewicza 30, 30-059 Kraków, Poland

autor

Szwed P.

• AGH University of Science and Technology, al. Mickiewicza 30, 30-059 Kraków, Poland

Bibliografia

• [1] 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.
• [2] 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.
• [3] 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.
• [4] 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.
• [5] van Benthem J.: Temporal Logic. [in:] Handbook of Logic in Artificial Intelligence and Logic Programming. vol. 4, Clarendon Press 1993-95, pp. 241-350.
• [6] Clarke E.M. Jr., Grumberg O., Peled D. A.: Model Checking. MIT Press 1999.
• [7] Cockburn A.: Writing Effective Use Cases. Addison-Wesley 2001.
• [8] D'Agostino M., Gabbay D.M., Halinie R., Posegga J. (eds): Handbook of Tableau Methods. Kluwer Academic Publishers 1999.
• [9] 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.
• [10] Fowler M.: UML Distilled. 3rd Edition. Addison-Wesley 2004.
• [11] Hurlbut R.: A survey of approaches for describing and formalizing use-cases. Technical Report 9703, Department of Computer Science, Illinois Institute of Technology 1997.
• [12] 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.
• [13] Klimek R., Skrzyński P., Turek M.: Automatic verification of the model at the requirements analysis phase [in Polish]. 12th National Conference of Software Engineering, Poland, Gdańsk, September 27-29, PWNT 2010, pp. 209-216.
• [14] Kósters 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.
• [15] Król T.: The simulation of use cases [in Polish]. Master thesis (superviser: R. Klimek). AGH University of Science and Technology 2007.
• [16] 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.
• [17] Reisig W.: Petri Nets - An Introduction. (EATCS Monographs on Theoretical Computer Science, Volume 4). Springer Verlag 1985.
• [18] Saeki M., Kaiya H., Hattori S.: Applying a Model Checker to Check Regulatory Compliance of Use Case Models. Proc. of CAiSE Forum 2009.
• [19] Shen W., Liu S.: Formalization, Testing and Execution of a Use Case Diagram. ICFEM 2003 International Conference on Formal Engineering Methods, Singa-pore, 2003. (Lecture Notes in Computer Science, 2885), Springer Verlag 2003, pp. 68-85.
• [20] 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.