Zastosowanie weryfikacji dedukcyjnej w projektowaniu oprogramowania korporacyjnego budowanego w oparciu o paradygmat SOA

• Autorzy: Radosław Klimek , Paweł Skrzyński

Warianty tytułu

Deduction Based Formal Verification of SOA Compliant Enterprise Software

• Języki publikacji: PL

Abstrakty

Praca dotyczy zagadnień modelowania i weryfikowania oprogramowania korporacyjnego, budowanego zgodnie z architekturą SOA. Zostały pokazane możliwości budowy takiego oprogramowania w oparciu o środowisko zorientowane na usługi. Przedstawiono zarys odpowiedniej metodyki modelowania. Język modelowania procesów biznesowych BPMN może być uznany za język wizualizacji środowiska usług sieciowych. Procesy takie mogą i powinny być zweryfikowane pod względem formalnej poprawności. Dobre możliwości weryfikacji daje tutaj podejście dedukcyjne z wykorzystaniem logiki modalnej i metody tablic semantycznych jako metody wnioskowania. Przedstawiono możliwości automatycznej budowy specyfikacji logicznej z wzorców projektowych BPMN, co ma kluczowe znaczenie w przypadku budowy modelu logicznego rzeczywistego systemu. (abstrakt oryginalny)

EN

The work concerns the issues of modelling and verification of enterprise software which is built according to SOA principles. The possibility of building such software is shown. An appropriate modelling methodology is outlined. Business process modelling notation (BPMN) can be considered as a visualization language of web services. Such processes can and should be verified in a formal way. Deductive approach using modal logic and semantic tableaux method gives a good opportunity for such formal verification. The possibility of automatic construction of a logical specification is presented. This automatic construction is based on design patterns of BPMN. (original abstract)

Słowa kluczowe

PL

Oprogramowanie; Architektura zorientowana na usługi SOA; Modele biznesowe; Logika

EN

Software; Serviced Oriented Architecture; Business models; Logic

• Czasopismo: Prace Naukowe Uniwersytetu Ekonomicznego we Wrocławiu. Informatyka Ekonomiczna
• Rocznik: 2011
• Tom: 22
• Numer: nr 212
• Strony: 184--195

Twórcy

autor

Radosław Klimek

• AGH Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

autor

Paweł Skrzyński

• AGH Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

Bibliografia

• Business Process Modelling Notation, V 2.0, OMG Document Number: formal/2011-01-03, URL: http://www.omg.org/spec/BPMN/2.0.
• Ertl T. [2008], SOA Design Patterns, Prentice Hall. New Jersey.
• D'Agostino M., Gabbay D.M., Hahnle R., Posegga J. (eds) [1999], Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht.
• Juric M.B., Krizevnik M. [2010], Overview of WS-BPEL 2.0 for SOA Composite Applications with Oracle SOA Suite 11g, Packt Publishing. http://www.packtpub.com/sites/default/files/7948- chapter-9-bpel-with-oracle-service-bus-and-service .pdf.
• Klimek R. [1999], Wprowadzenie do logiki temporalnej, Wydawnictwa Naukowo-Techniczne AGH, Kraków.
• Klimek R. [2011], Weryfikacja procesów biznesowych metodą dedukcyjną z wykorzystaniem logiki temporalnej, "Pomiary Automatyka Robotyka", nr 12, s. 190-193.
• Klimek R., Skrzyński P., Turek M. [2010], Deduction based verification of business models, [w:] Advanced Information Technologies for Management, eds. J. Korczak, H. Dudycz, M. Dyczkowski (Research Papers of Wroclaw University of Economics no. 147), Publishing House of Wroclaw University of Economics, Wrocław, s. 173-188.
• Maréchaux J.L., Combining Service-Oriented Architecture and Event-Driven Architecture using an Enterprise Service Bus, IBM technical paper, http://www.ibm.com/developerworks/library/wssoa- eda-esb/.
• Rosen M. [2008], Orchestration Or Choreography?, www.bptrens.com, April.
• van der Aalst W.M.P., ter Hofstede A.H.M., Kiepusewski B., Barros A.P. [2003], Workflow Patterns, "Distributed and Parallel Databases", 4(1), s. 5-51.