Zastosowanie weryfikacji dedukcyjnej w projektowaniu oprogramowania korporacyjnego budowanego w oparciu o paradygmat SOA - Klimek, Radosław; Skrzyński, Paweł (Deduction based formal verification of SOA compliant enterprise software, 2011)
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.
Prace Naukowe Uniwersytetu Ekonomicznego we Wrocławiu = Research Papers of Wrocław University of Economics; 2011; Nr 212, s. 184-195
Keywords: oprogramowanie korporacyjne; SOA; modelowanie biznesowe; BPMN; weryfikacja formalna; logika temporalna; logika epistemiczna; metoda tablic semantycznych; eneterprise software; Service Oriented Architecture; business modeling; formal verification; temporal logic; epistemic logic; semantic tableaux method