Weryfikacja aktywności systemów modelowanych na bazie architektury SOA - prowadzona w oparciu o wymagania zadane diagramami przypadków użycia

• Autorzy: Klimek R. , Skrzyński P. , Turek M.

Warianty tytułu

EN

Verification of activity for SOA-based systems - carried out on a use-case diagrams requirements

• Języki publikacji: PL

Abstrakty

PL

Artykuł porusza zagadnienia formalnej weryfikacji wymagań dla tzw. systemów biznesowych, wyrażonych przez model przypadków użycia oraz scenariuszy przypadków użycia UML. Zaproponowana została metodologia opisująca przejście od diagramów przypadków użycia do diagramów aktywności. Do specyfikacji żądanych własności systemu została wykorzystana logika temporalna. Własności tak zakodowane mogą być następnie poddawane procesom weryfikacji z wykorzystaniem wnioskowania dedukcyjnego metodą tablic semantycznych. Zaproponowane zostały metody pozyskiwania formuł logiki temporalnej bezpośrednio ze scenariuszy przypadków użycia zapisanych w diagramach czynności UML.

EN

The article discusses the issue of f formal requirements verification for so-called "business systems" - expressed through an UML Use-Case model and Use-Case scenarios. A methodology for transformation of UML Use-Case diagrams to Activity diagrams has been described. To specify advanced system requirements a temporal logic notation was used. These requirements (encoded in such way) could be verified with a deductive inference based on semantic tables. The methods for obtaining temporal logic formulas directly from Use-Case scenarios stored in the UML Activity diagrams have also been introduced.

Słowa kluczowe

PL

weryfikacja; logika temporalna; architektura SOA; diagramy UML; przypadki użycia; narzędzia UML; translacja diagramów UML

EN

veriflcation; temporal logic; SOA architecture; UML diagrams; use-case; UML Tools; UML Diagram Translation

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
• Rocznik: 2010
• Tom: T. 14, z. 3/2
• Strony: 893--903
• Opis fizyczny: Bibliogr. 5 poz., rys.

Twórcy

autor

Klimek R.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

autor

Skrzyński P.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

autor

Turek M.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

Bibliografia

• [1] D’Agostino M., Gabbay D.M., Hahnle R., Posegga J. (eds), Handbook of Tableau Methods. Kluwer Academic Publishers, 1999.
• [2] Booch G., Rumbaugh J., Jacobson I., The Unified Modeling Language User Guide. Addison-Wesley, 1998.
• [3] van Benthem J., Temporal Logic. Handbook of Logic in Artificial Intelligence and Logic Pro gramming, vol. 4, 241-350, Clarendon Press 1993-95.
• [4] Emerson E.A., Temporal and Modal Logic. Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics. MIT Press, Elsevier, 1990, 995-1072.
• [5] Eshuis R., Wieringa R., Tool Supportfor Ferifying UML Activity Diagrams. IEEE Transactions on Software Engineering, vol. 30, No. 7, 437-447.