@misc{Klimek_Radosław_Zastosowanie_2011, author={Klimek, Radosław and Skrzyński, Paweł}, year={2011}, rights={Wszystkie prawa zastrzeżone (Copyright)}, description={Prace Naukowe Uniwersytetu Ekonomicznego we Wrocławiu = Research Papers of Wrocław University of Economics; 2011; Nr 212, s. 184-195}, publisher={Wydawnictwo Uniwersytetu Ekonomicznego we Wrocławiu}, language={pol}, abstract={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.}, title={Zastosowanie weryfikacji dedukcyjnej w projektowaniu oprogramowania korporacyjnego budowanego w oparciu o paradygmat SOA}, type={artykuł}, 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}, }