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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
Budapesti Műszaki és Gazdaságtudományi Egyetem
BPEL alapkoncepció
Fault Tolerant Systems Research Group
4
Budapesti Műszaki és Gazdaságtudományi Egyetem
Web szolgáltatások
Fault Tolerant Systems Research Group
5
Budapesti Műszaki és Gazdaságtudományi Egyetem
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>
Fault Tolerant Systems Research Group
6
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
7
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
8
9
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
Event Handler 1 Event Handler 2
Budapesti Műszaki és Gazdaságtudományi Egyetem
Hibakezelés a BPEL nyelvben 1
Scope: tevékenységek egy sorozata melyre definiálható Faulthandler Compensation handler Scope is tartalmazhaz scope-ot
Fault Tolerant Systems Research Group
10
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
13
Budapesti Műszaki és Gazdaságtudományi Egyetem
Munkafolyamatok ellenőrzése Tranzíciós rendszer • Absztrakt adatok
Fault Tolerant Systems Research Group
14
Budapesti Műszaki és Gazdaságtudományi Egyetem
Munkafolyamatok ellenőrzése Tranzíciós rendszer • Absztrakt adatok
Követelmények • LTL: lineáris temporális logika Fault Tolerant Systems Research Group
15
16
Budapesti Műszaki és Gazdaságtudományi Egyetem
Munkafolyamatok ellenőrzése Tranzíciós rendszer • Absztrakt adatok
Követelmények • LTL: lineáris temporális logika Fault Tolerant Systems Research Group
Modellellenőrző • LTL kifejezések formális helyességellenőrzése • Kimerítő állapottérbejárás
17
Budapesti Műszaki és Gazdaságtudományi Egyetem
Munkafolyamatok ellenőrzése Tranzíciós rendszer • Absztrakt adatok
Modelltranszformáció Modelltranszformáció VIATRA2 keretrendszer • gráftranszformáció • absztrakt állapotgépek
Követelmények • LTL: lineáris temporális logika Fault Tolerant Systems Research Group
Modellellenőrző • LTL kifejezések formális helyességellenőrzése • Kimerítő állapottérbejárás
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
18
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
Változók modellezése Inicializálatlan
Olvasva
Írva
Írva és olvasva
Ellenőrzés: folyamat |- G(változó /= írva);
Fault Tolerant Systems Research Group
21
Budapesti Műszaki és Gazdaságtudományi Egyetem
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)
Fault Tolerant Systems Research Group
22
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
23
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Fault Tolerant Systems Research Group
25
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
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
Budapesti Műszaki és Gazdaságtudományi Egyetem
Köszönöm a figyelmet!
Fault Tolerant Systems Research Group
28