BPEL nyelvű üzleti folyamatok modellezése és formális ellenőrzése

Budapesti Műszaki és Gazdaságtudományi Egyetem

BPEL nyelvű üzleti folyamatok modellezése és formális ellenőrzése

Kovács Máté, Gönczy László {kovmate,gonczy}@mit.bme.hu Budapesti Műszaki és Gazdaságtudományi Egyetem Méréstechnika és Információs Rendszerek Tanszék Research suported by Software Engineering for Service-Oriented Overlay Computers (SENSORIA) EU FET-IST project. Fault Tolerant Systems Research Group

2


Munkafolyamatok végrehajtása Hagyományos Regisztrálás

Elektronikus Típus besorolás

Papír

Típus besorolás

Regisztrálás

Elutasíás

Kifizetés

Fault Tolerant Systems Research Group

Szerődés Munkafolyamat végrehajtó motor

Szerződés

Egyenleg

Web szolgáltatás hívás

Egyenleg

Kifizetés

Elutasítás

3


Munkafolyamat példa A párhuzamos végrehajtás kezdete

Egyszerű tevékenység

Regisztrálás

Elágazás

Szerződés

Elutasítás

Egyenleg

Fizetés

Típus besorolás

Vezérlési folyam

A párhuzamos végrehajtás vége



BPEL alapkoncepció


4


Web szolgáltatások


5


A BPEL elemei Process felépítése <partnerLink> - Kapcsolat két szereplő közt <partner> - partnerLink-ek halmaza - folyamat globális változói, ideértve a kimenő/bejövő üzeneteket - folyamat lépései Egyéb elemek: , , , <eventHandler>


6


A BPEL elemei 2. Basic activity - Web service meghívása - Web service funkcionalitás a hívó fél felé - belső hiba jelzése (kivétel) <wait> - várakozás - változók elérése/kezelése - compensationHandler hívás sikeresen lefutott lépés visszavonása


7


A BPEL elemei 3. Structured activity <sequence> - sorosan végrehajtandó lépések <switch> - feltételes elágazás <while> - ciklus - üzenetek, alarmok kezelése - párhuzamosan végrehajtható tevékenységek


8

9


Scope Scope

Regisztrálás

Elutasítás

Egyenleg

Fizetés

Típus besorolás

Fault Hanlder 1 Fault Hanlder 2

Szerződés

Compensation Handler


Event Handler 1 Event Handler 2


Hibakezelés a BPEL nyelvben 1

Scope: tevékenységek egy sorozata melyre definiálható Faulthandler Compensation handler Scope is tartalmazhaz scope-ot


10


Hibakezelés a BPEL nyelvben 2 Kivételes esemény: Fault Invoke dobja Throw tevékenység dobja Faulthandler kapja el Ha nincs megfelelő faulthandler: tartalmazott scope-ok kompenzálása a fault továbbdobása a tartalmazó scope felé

Kompenzálás Sikeresen végrehajtott scope kompenzálható A compensation handler snapshot világban él Ha nincs compensation handler: A tartalmazott scope-ok kompenzálása Fault Tolerant Systems Research Group

11


Motiváció Web szolgáltatások kompozíciója széleskörű eszköztámogatás Probléma: munkafolyamatok tesztelése Az adatok távoli adatbázisokban vannak A tesztfuttatások hatását érvényteleníteni kell Megoldás: munkafolyamatok formális analízise A munkafolyamatok formalizálása A formális modell tulajdonságainak ellenőrzése Szimuláció, Hibaszimuláció Fault Tolerant Systems Research Group

12


Már létező megoldások W. van der Aalst: munkafolyamat modellezés Petri hálókkal Shin Nakajima: WSFL majd BPEL flow vizsgálata Sebastian Hinz et. al.: BPEL Petri háló Kovács Máté, Gönczy László: BPEL adatfolyam hálók


13


Munkafolyamatok ellenőrzése Tranzíciós rendszer • Absztrakt adatok


14



Követelmények • LTL: lineáris temporális logika Fault Tolerant Systems Research Group

15

16




Modellellenőrző • LTL kifejezések formális helyességellenőrzése • Kimerítő állapottérbejárás

17



Modelltranszformáció Modelltranszformáció VIATRA2 keretrendszer • gráftranszformáció • absztrakt állapotgépek


Modellellenőrző • LTL kifejezések formális helyességellenőrzése • Kimerítő állapottérbejárás


Modellellenőrzés

Ellenőrzés: Modell: tranzíciós rendszer Követelmény: lineáris temporális logikai kifejezés Eredmény: a követelmény igazságtartalma a modellen


18


Modellellenőrzés Tranzíciós rendszer: Állapotváltozók Állapot átmeneti szabályok

(feltétel) értékadások; szintaktikával

Az állapottér az állapotváltozók értékkészletének Descartes szorzatának azon részhalmaza, amely elérhető a kiindulási állapotból a tranzíciók mentén.

Lineáris Temporális Logikai kifejezés: A nulladrendű logika + temporális operátorok: Gp: Fp: Xp: pUq: Fault Tolerant Systems Research Group

19

20


Változók modellezése Inicializálatlan

Olvasva

Írva

Írva és olvasva

Ellenőrzés: folyamat |- G(változó /= írva);


21


Egyszerű tevékenységek modellezése Nem indítható

Befejezett

Indítható

Változó Olvasva

Ellenőrzés: folyamat |- F(válasz=befejezett) OR F(visszagörgetés=befejezett)


22


Strukturált tevékenységek modellezése … <sequence>

… sequence=fut AND invoke_a=nem_indítható invoke_a=indítható; sequence=fut AND invoke_b=nem_indítható AND invoke_a=befejezett invoke_b=indítható; sequnece=fut AND invoke_b=befejezett sequence=befejezett;

Nem indítható

Befejezett

Indítható

Fut


23


A Scope modellezése Indítható

Nem indítható

Hibakezelés

Fut

Kompenzálható

Hibásan befejezett

Kompenzálás

Kompenzált

Minden nem indítható – indítható átmenetnél ellenőrizzük, hogy az összes tartalmazó scope megfelelő állapotban van-e. Fault Tolerant Systems Research Group


Scope állapotára vonatkozó indítási feltételek

… AND scope_1=hibakezelés AND scope2=kompenzálás AND scope_3=fut AND … Fault Tolerant Systems Research Group

24


Hibaszimuláció A hiba terjedése változókban: két új állapot: hiba írva, hiba írva és olvasva a jelenlegi implementáció tartalmazza

A vezérlés hibájának modellezése: egymásnak ellentmondó követelmények: szemantika hű leképezése hibás pozitív eredmény elkerülése


25


Megvalósítás Modelltranszformációs motor: VIATRA2 gráftranszvormációs keretrendszer deklaratív és imperatív programozási paradigmák ötvözése

A kód hossza: 6077 sor +BPEL importer +WSDL importer +SAL generátor Fault Tolerant Systems Research Group

26


27

Konklúzió és továbbfejlesztési lehetőségek Konklúzió: siker: gyakorlatban is alkalmazható munkafolyamat verifikációs metodika Továbbfejlesztési lehetőségek: Általános követelmények automatikus generálása: Egyetlen inicializálatlan változót sem olvasunk Szinkron munkafolyamat esetén mindenképp szolgálunk visszatérési értékkel

Teljes Web szolgáltatás alapú környezet vizsgálata a folyamatok direktszorzatával "Back annotation" a munkafolyamatra Fault Tolerant Systems Research Group


Köszönöm a figyelmet!


28

BPEL nyelvű üzleti folyamatok modellezése és formális ellenőrzése

Recommend Documents