Pannon Egyetem Műszaki Informatikai Kar Tézisfüzet Elosztott rendszerek formális modelleken alapuló tervezési eljárásainak vizsgálata
írta: Jaskó Szilárd Konzulensek: Dr. Tarnay Katalin Dr. Simon Gyula Informatikai Tudományok Doktori Iskola Pannon Egyetem 2012
1 A kutatás előzménye és célkitűzése Kutatásom célja olyan eljárások és modellek kidolgozása, amelyek segítségével hatékony, újrakonfigurálható, adaptív, illetve strukturálisan holtpontmentes elosztott rendszerek hozhatók létre. Az új eljárások kidolgozása formális nyelveken alapul, amelyek segítségével hatékonyan támogatni lehet az elosztott rendszerek, vagy azok egyes elemeinek specifikálását és verifikálását. Modellek esetében célom olyan matematikai leírás megalkotása, amely alkalmas elosztott rendszerek modellezésére, ezeknek a rendszereknek a specifikálására és egyben programozására is, valamint amelyek segítségével új típusú újrakonfigurálható és adaptív megvalósítások jönnek létre. A cél érdekében végzett kutatási munka négy fő részre osztható: (1) Az elosztott rendszerek egyes elemei közötti kommunikáció szempontjából fontos az ITU-T (International Telecommunications Union - Telecommunication Standardization Sector) nemzetközi szervezet által szabványosított URN (User Requirements Notation) egy új felhasználási módjának a kidolgozása, amely a protokolltervezés legköltségesebb részének, a tesztelésnek, illetve ennek egyes elemeinek specifikálására alkalmas. (2) Egy új self-adaptív kommunikációs rendszermodell kifejlesztése, amely formális specifikáción keresztül definiálja a rendszer kommunikációs szabályszerűségeit, a környezet hatására képes más kommunikációs viselkedési sémára váltani és a formálisan specifikált protokollhalmazt a rendszer szinkronizálni tudja. (3) Egy olyan új elosztott/beágyazott rendszermodell kifejlesztése, amely strukturálisan holtpontmentes, kis erőforráskészletű rendszerek esetén is alkalmazható és a rendszerben felmerülő folyamatok, illetve részfolyamatok specifikálására és programozására egy specifikáció-közeli, új matematikai alapokon nyugvó formalizmust használ. (4) A CSP (Communicating Sequential Processes) formális nyelvből származtatott CSCSP (Controlled Signal CSP) létrehozása, amely moduláris rendszerű, az egyes elemei újrafelhasználhatóak
és
egybeépíthetőek,
valamint
strukturálisan
garantálható
a
holtpontmentes modulokból származtatott új modulok holtpontmentessége. A fent tárgyalt négy terület kutatási előzményét és a rövid bemutatását a következő rész tárgyalja.
1.1 Az URN és a tesztelés kapcsolata Az URN a távközlési szoftverek követelmény-menedzselésével foglalkozó nyelv. Az ITU-T a Z.150 [H1] szabványban specifikálja a nyelvvel kapcsolatos követelményeket és a Z.151 [H2] szabványban foglalkozik a nyelv definiálásával. Az URN két részből áll, a nem-funkcionális
2
célorientált nyelvből, a GRL-ből (Goal-oriented Requirement Language) és a funkcionális, használati eseteket specifikáló UCM-ből (Use Case Maps) [H3]. Az URN-el kapcsolatos kutatások két fő részre oszthatók. Az egyik irányzat az URN új területen
való
alkalmazása/alkalmazhatósága,
illetve
összetevői
tulajdonságainak
a
kiterjesztése. A másik kutatási irány az URN kapcsolatát vizsgálja más formális nyelvekkel, illetve eszközökkel. Az URN-el kapcsolatos, alig 10 éves kutatások megmutatták, hogy az URN használható a teljesítmény követelmény specifikálásában [H4], a web alapú rendszerek tervezésében [H5] és az e-kereskedelemben [H6]. Az URN funkcionális részét, az UCM-et, valós idejű rendszerek leírására alkalmas módon kiterjesztették [H7], [H8], míg a GRL viszonyát másik célorientált és általános nyelvekkel kapcsolatban vizsgálták meg (például a KAOS-al és az UEML-el (Unified Enterprise Modelling Language)) [H9]. Kutatások során rávilágítottak arra, hogy a GRL alkalmas lehet üzleti stratégiák [H10] és hitelesítési, valamint azonosítási menedzsment folyamatok specifikálására [H11]. Az URN folyamatos fejlődésének eredményeképpen megszületett az URN aspektus orientált változata [H12]. Az URN használhatóságát befolyásolja, hogy a GRL-ben és az UCM-ben specifikált rendszerek leírását milyen más formális nyelvek, illetve eszközök irányában lehet transzformálni. Az URN kapcsolatban áll az MSC-vel (Message Sequence Chart), SDL-el (Specification and Description Language), UML-el (Unified Modeling Language), a TTCN-3al (Testing and Test Control Notation version 3), i* framework-kel, jUCMNav-al, UPPAALal, GME-vel, Tau G2-vel, és még számos formális nyelvvel és eszközzel [H13], [H14], [H15], [H16], [H17], [H18], [H19], [H20], [H21]. A tesztelés vonatkozásában eddig külön vizsgálták az URN két komponensét, azaz az UCM-et és a GRL-t. Az UCM elsődlegesen alkalmazások specifikálására való, de használták már egyes alkalmazások funkcionális ellenőrzésére is (például web alapú alkalmazások [H22]). A tesztelés során gyakran az UCM-ben leírt specifikációt más nyelvekké konvertálják (mint pl. MSC-Message Sequence Chart) [H23]. Hasonlóan a GRL esetén is a kutatások a hangsúlyt már létező, a verifikáció és rendszerhelyesség-ellenőrzés területén népszerű nyelvek irányába történő konverzióra helyezték [H9], [H17], [H21], [H24]. Célom megmutatni, hogy a GRL leírás alkalmas a teszt-terv során definiált teszt-cél, felhasznált módszer, elvégzendő feladat, erőforrás és lehetséges veszélyforrás specifikálására, valamint az UCM-mel kapcsolatos korábbi kutatások által nem vizsgált protokoll-tesztben résztvevő komponensek, azok viszonyának és interfészeinek leírására.
3
1.2 Self-adaptív kommunikációs rendszerek A self-adaptív elgondolást egyre több területen integrálják a meglévő, illetve az új rendszerekbe. Az adaptív rendszerekhez képest a self-adaptív megoldások nem csak a környezetüket monitorozzák, hanem a saját viselkedésüket is figyelembe veszik az adaptációs folyamat során. A self-adaptivitást felhasználják például az ipari gyártórendszerek esetén [H25], [H26], [H27], az orvostudomány területén [H28], a tudás alapú rendszereknél [H29], [H33], kémiai folyamatoknál
[H30],
áramkörök
tervezésénél
és
üzemeltetésénél
[H31],
[H32],
gyógyszergyártás területén [H34], erőforrás menedzselő rendszereknél [H35] és vízellátó rendszerek [H36] esetében. Napjainkra a self-adaptív technológia szinte az összes ipari alkalmazás területén használatban van, vagy vizsgálják annak használhatóságát. A telekommunikációhoz szorosabban kapcsolódó kutatásokat végeznek a következő területeken: vezeték nélküli megvalósítások rendszermenedzsmentjénél [H37], [H38], interfészek
tervezésénél
alkalmazásoknál
[H42],
[H39],
[H40],
hálózatok
middleware
útvonalválasztási
rendszereknél problémáinál
[H41], [H43]
web és
a
protokolltervezésnél [H44], [H45], [H46], [H47]. Minden olyan rendszer esetében, ahol csomópontok kommunikálnak egymással létjogosultsága lehet self-adaptív protokollok alkalmazásának. Célom (1) egy új formalizmus kidolgozása, amely képes self-adaptív kommunikációs viselkedések leírására, (2) az új formalizmushoz egy új végrehajtási környezet modelljének megalkotása, amely további transzformációs lépések nélkül képes végrehajtani az új formalizmussal leírt kommunikációs funkcionalitást, (3) a rendszer verifikálása, különös tekintettel a self-adaptivitás és tesztelhetőség követelményeire.
1.3 Masszívan elosztott eseményvezérelt rendszerek A masszívan elosztott rendszerekben, akár több ezer csomópont párhuzamos és koordinált működése szolgáltatja az elvárt viselkedést. Egy tipikus és gyorsan fejlődő ilyen irányzat a szenzor hálózatok területe. Az első szenzor hálózatokat 1998-ban hozták létre a „Smartdust” program keretei között [H48]. A fontosabb kutatások rendszerezve megtalálhatóak a Berkeley WEBS (Wireless Embedded Systems) [H49] és a CENS (Center for Embedded Networked Sensing) [H50] weboldalakon. A szenzor hálózatok felhasználási területe nagyon sokrétű. Az egyik fő kutatási ág a környezetvédelem, ahol például állatok viselkedését figyelik meg [H51], [H52], vagy a tűzvészeket és a földrengéseket monitorozzák és jelzik [H53]. Egy másik nagy felhasználási
4
terület az ipari rendszerek, ebben az esetben a szenzorok mérhetnek forgalommal, bányászattal, épület/építmény állapotával, vízgazdálkodással, vagy levegő felhasználással kapcsolatos adatokat [H54], [H55], [H56], [H57], [H58]. A következő fő terület az alkalmazások vonatkozásában az egészségügyi felhasználás, mint például a Code Blue kutatás, ami a sürgősségi betegellátás monitorozásában és adatgyűjtésében segít [H59], de alkalmas még szívmonitorozásra [H60], [H61] és az izomműködés megfigyelésére [H62] is. Lehetőség van a szenzorok segítségével az otthonunk monitorozására [H63]. A technológiának számos katonai felhasználása is van, ami például a szenzorhálózat segítségével határozza meg a mesterlövész helyzetét, [H64], [H65] vagy ellenséges aktivitásokat detektál (pl. line in the sand projekt [H66]). A jó minőségű alkalmazások létrehozásának feltétele a magas szintű midleware szolgáltatások jelenléte. Az elmúlt évek kutatásai során számos új módszer született, például az energiagazdálkodás [H67], az útmenedzsment [H68], a forgalomirányítás [H69], a lokalizáció [H70], a hibamenedzsment [H71], [H72] és a szinkronizáció [H73] problémáinak területén. A virtuális gép (VM, Virtual Machine) egy gyakran alkalmazott technológia. Ezt eredendően azért fejlesztették ki, hogy egy platformfüggetlen környezetet hozzon létre az operációs rendszer és a futtatási környezet között. Ez a technológia megjelent a szenzorhálózatok területén is. Az első ilyen alkalmazást a Berkeley kutatói fejlesztették ki és Maté-nak [H74] nevezték el. Ez a VM TinyOS [H78] operációs rendszer felett fut. Az elgondolásukat továbbfejlesztették, és egy sokkal flexibilisebben használható eljárást hoztak létre (Application Specific Virtual Machine) (ASVM) [H75]. Egy másik elképzelés a „SensorWare”, amely egy szkript nyelv [H76] és nem tekinthető igazi VM megvalósításnak. A VM* implementáció egy hibrid elképzelés, ami keveri a natív és a virtuális programozási kódot a processzor hatékonyabb kihasználása érdekében. A VM megvalósításoknak fő hátránya, hogy pazarlóbban bánnak az erőforrásokkal, mint a natív kódos megvalósítások [H77]. Célom (1) egy új redukált CSP-alapú formalizmus létrehozása, amely eseményvezérelt folyamatok formális specifikálására alkalmas, (2) egy új, elosztott környezetben működő platformfüggetlen végrehajtási környezet kidolgozása, amely további transzformációs lépések nélkül képes kezelni és végrehajtani az új redukált CSP alapú formalizmussal specifikált algoritmusokat,
(3)
és
az
új
környezetben
verifikálhatóságának biztosítása.
5
létrehozott
rendszerek
formális
1.4 A CSP és a CSP-ből származtatott nyelvek A Communicating Sequential Processes (CSP) nevű konkurens rendszerek specifikálására és verifikálására alkalmas matematikai leíró nyelvet C. A. R. Hoare publikálta [H79]. A CSP első sikerét a drága, nagy komplexitású rendszerek területén érte el. Ebben az időben kezdte el a Philips és kutatócsapata egy duális számítógép rendszer (Dual Computer System, DCS) megtervezését, hogy létrehozzanak egy nagy rendelkezésre állású adatbázis szervert. Az ilyen jellegű és bonyolultságú problémák specifikálására és verifikálására végül egy nagyon elegáns megoldás született 1987-ben Tony Hoare és He Jifeng tolmácsolásában [H80], amiben természetesen a CSP kapta a főszerepet. Fontos volt, hogy ez a tudományos eredmény demonstrálja a CSP-ben rejlő elméleti és gyakorlati lehetőségeket. A sikeres bemutatkozás után a CSP-t számos fontos területen alkalmazták a nemzetközi űrállomástól az Airbus A340 tervezéséig [H81]. A sokrétű felhasználhatóságon túl több verifikációs, szimulációs és elemző alkalmazást fejlesztettek ki a CSP-hez [H82], [H83], [H84]. A CSP felhasználásával, kiterjesztésével vagy szűkítésével kapcsolatban folyamatosan születnek új kutatási eredmények. Az R2D2C (Requirements to Design to Code) például módszertant biztosít a szóbeli specifikációtól a tervezésen keresztül a programkód létrejöttéig [H85]. Kutatások vizsgálják a CSP és a Z [H86], a CASL [H87], az object-Z [H88] és a B [H89] formális nyelvek kapcsolatát. A CSP-t axiomatikus szemantikával is kiegészítették [H90]. A CSP-vel kapcsolatos kutatások egyik irányzata a nyelv bővítésével biztosít nagyobb ábrázolási képességet – mint például az időzített CSP [H91], [H92], [H93], – míg mások a nyelv szűkítése mentén próbálják azt speciális területeken hatékonyabbá tenni, mint például a CSP-S [H94]. Célom egy olyan CSP-ből származtatott új CSP variáns létrehozása, amelyben a folyamatok modulárisak
és
a
korábban
definiált
modulok
felhasználásával
új
folyamatok
származtathatóak olyan módon, hogy a folyamatokból konstruált összetett új folyamatok holtpontmentessége garantálható legyen.
2 Módszerek Irodalomkutatatást végeztem a telekommunikáció, self-adaptivitás, formális nyelvek és a szenzorhálózatok területén. A publikált eredmények analízise során azonosítottam a kutatásaimhoz kapcsolódó létező megoldásokat és nyitott kérdéseket, valamint a lehetséges további kutatási irányokat, illetve az ezekben alkalmazható módszereket. Új módszertant definiáltam az URN és a CSP alkalmazására a protokolltesztelés és az elosztott rendszerek
6
holtpontmentes tervezésének területén. Új elosztott rendszermodelleket specifikáltam a CSP leíró nyelv segítségével. A modellek tulajdonságait matematikai eszközökkel vizsgáltam, állításaimat formális bizonyításokkal igazoltam. Elméleti állításaimat valós implementációk segítségével validáltam, a megvalósított fizikai rendszerek tulajdonságait teszteléssel, valamint műszeres mérésekkel ellenőriztem. Munkám során két formális nyelvvel, valamint az implementáció során használt fejlesztő és futtatási környezetekkel dolgoztam. A felhasznált formális nyelvek az URN és a CSP, míg az alkalmazott programozási nyelvek a JAVA, Python és a nesC voltak. A tesztelés során TinyOS fejlesztési és szimulációs környezetet, valamint micaZ szenzorhálózati eszközöket alkalmaztam. A műszeres méréseket digitális oszcilloszkóp segítségével végeztem el.
3 Új tudományos eredmények összefoglalása 1. tézis: Új módszertant dolgoztam ki a protokoll-tesztek specifikációjának területén, amely segítségével szerkezeti átalakítás nélkül kibővíthető az URN (User Requirements Notation) ITU-T (International Telecommunications Union - Telecommunication Standardization Sector) szabvány felhasználási spektruma. Az URN a GRL (Goaloriented Requirement Language) nem funkcionális és az UCM (Use Case Map) funkcionális leírási részekből áll. A tézishez kapcsolódó publikációk: [S1], [S3], [S5], [S9]. A témakör részletesen tárgyalásra kerül a PhD disszertáció 3. fejezetében. 1.1. Megmutattam, hogy a GRL alkalmas változatlan szintaktikával a teszt-terv meghatározására, azaz a GRL segítségével a tesztelés céljai, felhasznált módszerei, az elvégzendő feladatok, erőforrások és a lehetséges veszélyforrások specifikálhatók. 1.2. Megmutattam, hogy az UCM alkalmas változatlan szintaktikával a protokolltesztekben résztvevő komponensek (TC - Test Component, IUT - Implementation Under Test, Felső teszter, Alsó teszter), azok kapcsolatának (architektúrájának), a PCO-knak (Point of Control and Observation) és a CP-knek (Coordination Point) a specifikálására.
2. tézis: Új formalizmust dolgoztam ki a csomópontok közötti kommunikációt definiáló protokollhalmazok leírására. Definiáltam egy új végrehajtási modellt, amely értelmezi, aktiválja, inaktiválja és törli a protokollhalmaz egyes elemeit, valamint csomópont- és rendszerszintű menedzsment folyamatokat biztosít. A tézishez kapcsolódó publikációk:
7
[S4], [S16], [S17]. A témakör részletesen tárgyalásra kerül a PhD disszertáció 4. fejezetében. 2.1. Új formalizmust és modellt dolgoztam ki. A formalizmus alkalmas a self-adaptív kommunikációs viselkedés leírására, amely formális specifikáción keresztül lehetővé teszi, hogy különböző állapotokhoz különböző viselkedési sémákat rendeljünk hozzá. A modell ezt a formalizmust hasznosítja, amelynek a CSP alapú Kommunikációs Modell (Communicating Sequential Processes based Communication Model – CSPBCM) nevet adtam. A CSP-BCM az új formalizmussal specifikált kommunikációs szabályokat további transzformációs lépések nélkül képes végrehajtani, és menedzsment folyamatokat biztosítani azok terjesztésére, szinkronizációjára, tesztelésére és törlésére, illetve az egyes protokollok aktiválására és inaktiválására. Megmutattam, hogy a CSP-BCM rendszer az új formalizmus alkalmazása esetén selfadaptív tulajdonságokkal rendelkezik. 2.2. Létrehoztam az elméleti modellnek egy implementációját. Az implementáció keretei között igazoltam, hogy a mintaillesztési technika alkalmazható az új formalizmus elemei közötti egyezőség vizsgálatára, valamint megmutattam, hogy az új formalizmus tartalmazza a tesztesetek létrehozásához szükséges információt. Megjegyzés: Az altézis megértését segíti a PhD disszertáció 4. fejezetében található 11. összegző táblázat.
3. tézis: Új, redukált CSP-alapú formalizmust és új platform-független végrehajtási környezetet hoztam létre, amelyek az eseményvezérelt rendszerek specifikációjára, illetve a specifikált funkciók további transzformációs lépések nélküli végrehajtására alkalmasak. Igazoltam, hogy az általam definiált formalizmussal leírt, az általam definiált végrehajtási környezetben futatott kód strukturálisan holtpontmentessé tehető. A tézishez kapcsolódó publikációk: [S2], [S8]. A témakör részletesen tárgyalásra kerül a PhD disszertáció 5. fejezetében. 3.1. Új, redukált CSP-alapú formalizmust hoztam létre. Az új formalizmus elemi egysége a funclet, ami egy eseményvezérelt funkcionalitás leírását tartalmazza. A funclet alkalmas az elosztott/beágyazott rendszerekben felmerülő folyamatok, illetve részfolyamatok specifikálására. Megmutattam, hogy a funclet-alapú leírás hatékonyan alkalmazható
alkalmazások
leírására
újrakonfigurálható rendszerekben.
8
kis
erőforráskészletű,
beágyazott,
3.2. Új, elosztott környezetben működő platform-független végrehajtási környezetet (CSP-VM) dolgoztam ki, amellyel az új redukált CSP-alapú formalizmusban specifikált leírás további transzformációs lépések nélkül végrehajtható. Megadtam a CSP-VM, az elosztott/beágyazott rendszer elemeinek, valamint a rendszer elemei közötti kommunikációnak – a funcletek leírásával kompatibilis – egységes matematikai leírását. Gyakorlati alkalmazások segítségével igazoltam, hogy a funcletre és a CSP-VM-re épülő alkalmazások futás idejű újrakonfigurálása hatékonyan és flexibilisen történik. 3.3. Igazoltam a strukturális holtpontmentességet, a funcleteket futtató CSP-VM alapú csomópont és az egész hálózat vonatkozásában, ha bármely aktiválódott funclet a rendszerben lévő globális változóktól és a beérkező trigger eseményektől függetlenül véges időn belül lefut.
4. tézis: Új CSP-ből származtatott CSP variánst hoztam létre, amit vezérjeles CSP-nek (CSCSP, controlled signal CSP) neveztem el. A CSCSP elemi és származtatott folyamatai modulárisan egymásba építhetőek és újrafelhasználhatóak. Definiáltam egy új módszert, amelynek segítségével holtpontmentes CSCSP folyamatokból holtpontmentes kompozit folyamatokat lehet származtatni. A tézishez kapcsolódó publikációk: [S5], [S9], [S12], [S13], [S14]. A témakör részletesen tárgyalásra kerül a PhD disszertáció 6. fejezetében. 4.1. Új CSP-ből származtatott CSP variánst hoztam létre, és elégséges feltételt adtam holtpontmentes CSCSP folyamatokból garantáltan holtpontmentes összetett CSCSP folyamatok konstruálási szabályaira. Az új származtatott CSP variánsnak a vezérjeles CSP (CSCSP, Controlled Signal CSP) nevet adtam. Az autonóm CSCSP folyamatok egymással vezérjeleken keresztül szinkronizálódnak. Definiáltam a CSCSP folyamatokból összetett folyamatok konstruálásának szabályrendszerét, amellyel modulárisan egymásba ágyazható, ezáltal újrafelhasználható komponensek hozhatók létre. Bebizonyítottam, hogy amennyiben a holtpontmentes folyamatokat összekötő csatornák által meghatározott gráf körmentes, és az összes felhasznált folyamat ki- és bemenete a konstrukció során felhasználásra került, akkor a származtatott folyamat is holtpontmentes.
9
4 Alkalmazhatóság és továbbfejlesztés A kutatásom eredményeként létrejött (1) az URN szabványos formális nyelvvel kapcsolatban egy új módszertan, (2) egy új self-adaptív kommunikációs rendszermodell (CSP-BCM) és szoftveres megvalósítás, (3) egy új masszívan elosztott eseményvezérelt, strukturális holtpontmentességet biztosító rendszermodell (CSP-VM), valamint annak implementálása, (4) egy CSP-ből származtatott új CSP variáns, a CSCSP, amelynek elemei modulárisak, és a nyelv
szabályszerűségeit
felhasználva
biztosítja
a
származtatott
modulok
holtpontmentességét. Az URN a telekommunikáció területén szabványosított formalizmus. Az ipari és a kutató csoportok, az elterjedt gyakorlat alapján, a tervezés legelső lépésében használják. Kutatásom során feltártam, hogy az URN képes a teszt-tervet és néhány funkcionális teszteléssel kapcsolatos elemet specifikálni, azonban ez az általam kidolgozott gyakorlat az irodalomkutatás alapján eddig még nem került alkalmazásra az URN vonatkozásában. Az URN bevonása a tesztelés előkészítésébe egy másik fontos elvárással is egybecseng, ami azt mondja ki, hogy a lehető leghamarabb el kell kezdeni a tesztelés előkészítését és kifejlesztését. Ideális esetben a kész teszt-környezetnek rendelkezésre kellene állnia a protokoll elkészültekor. Minden eljárás, ami hatékonyabbá vagy olcsóbbá teheti a teszt kifejlesztési és lebonyolítási folyamatát – mivel a tesztelés a protokoll-tervezés teljes költségvetésének több mint felét emészti fel – a telekommunikáció számára kiemelten fontos. Az URN bevonása a teszt specifikációs folyamatába pontosan az előbb említett előnyökkel jár. A CSP-BCM elsősorban a telekommunikációs protokolltervezés, tesztelés és felhasználás területén nyújt új alkalmazási lehetőséget és módszert. A megvalósítás segítségével formálisan specifikált kommunikációs protokollhalmazt hozhatunk létre. A CSP-BCM megvalósítás ezt a formálisan specifikált leírást közvetlenül értelmezni és futtatni tudja, aminek a hatására a rendszerben specifikált kommunikációs formulákat nem kell implementálni a felhasználás előtt. A formális leírásnak egy másik gyakorlati haszna, hogy a csomóponton futó program kis költséggel elterjeszthető a hálózaton és szükség esetén ellenőrizhető mintaillesztési technikával, vagy a formális leírásból származtatott tesztelési eljárások segítségével. A kutatás során létrehozott demó alkalmazás megmutatta, hogy az elméleti elgondolás átültethető a gyakorlatba is. A CSP-VM megvalósítás alkalmazhatósága egyértelműen olyan rendszerekre korlátozódik, ahol az általam kifejlesztett eseményvezérelt formalizmus segítségével specifikálni lehet a 10
rendszer működését. Ilyen területek például az ipar számára is fontos szenzorhálózatok vagy a gyártó rendszerek. A kutatásom során a gyakorlati alkalmazás kiválasztásánál azért döntöttem a szenzorhálózatok mellett, mert azok erőforrásai erősen korlátozottak. Az elkészült implementáció bizonyítja, hogy az elméleti elgondolás ilyen típusú környezetben is alkalmazható. A virtuális gép-koncepció következtében más eseményvezérelt rendszerekbe is integrálható a CSP-VM, amennyiben a virtuális gép migrálása megtörténik az adott környezet irányába. A CSCSP származtatott formális nyelvet olyan rendszerek esetében célszerű használni, ahol a rendszer modulokból épül fel és a modulok interakcióban állnak egymással. Tipikusan ilyen terület például az elosztott rendszerek világa. További gyakorlati előnye a CSCSP megvalósításnak, hogy a korábban definiált holtpontmentes CSCSP folyamatokból bizonyított eljárásrend szerint szintén holtpontmentes új folyamat konstruálható. A kutatási eredmények két fő területen fejleszthetőek tovább: Az egyik a megvalósítások strukturális tulajdonságainak és összefüggéseinek további kutatása. Ilyen lehet például a holtpontmentesség mellett a végtelenciklus-mentesség kielemzése. A másik továbbfejlesztési lehetőség az eljárások és a modellek további konkrét alkalmazási területeinek meghatározása.
11
Saját publikációk Könyvek, könyvfejezetek: [S1]
Jaskó, Sz., Muhi D., Notations for test specification: TTCN3 and ASN.1. In: Advanced communication protocol technologies: solutions, methods and applications, in press Hershey, PA & New York, NY: IGI Global, pp. 57-77, 2011.
Referált idegen nyelvű folyóiratcikkek: Szilárd Jaskó, and Gyula Simon, „CSP-Based Sensor Network Architecture for Reconfigurable Measurement Systems,” IEEE Transactions on Instrumentation and Measurement, Vol. 60, No. 6, pp.2104 - 2117, June 2011. Impact factor (2009): 1.025 [S3] Szilárd Jaskó, Tibor Dulai, Dániel Muhi, Katalin Tarnay, „Test aspect of requirement specification,” Computer Standards and Interfaces, doi: 10.1016/j.csi.2008.12.005, vol. 32. Issues 1-2 . pp. 1–9., 2010. Impact factor (2010): 1.373 [S4] Szilárd Jaskó, Gyula Simon, Katalin Tarnay, Tibor Dulai, and Dániel Muhi, “CSPbased modelling for self-adaptive applications,” Infocommunications Journal, VOLUME LXIV, pp. 14-21, Feb. 2009. [S5] Szilárd Jaskó, “A new mathematical formalism for the ttcn 3 core language,” Periodica polytechnica ser. el. eng, vol. 49, no. 3, PP. 1–12., 2005. [S2]
Referált magyar nyelvű folyóiratcikkek: Jaskó Szilárd, Dr. Tarnay Katalin, „Tesztelés a telekommunikációban,” Híradástechnika pp. 12-16, Szept. 2006. [S7] Jaskó Szilárd, „Bluetooth Szolgáltatás Felfedező Protokoll “közérthető” ábrázolása,” Híradástechnika, pp. 39-45, Feb. 2002. [S6]
Nemzetközi referált konferencia kiadványában megjelent idegen nyelvű közlemények: [S8]
[S9] [S10]
[S11]
[S12] [S13]
S. Jaskó and G. Simon, „Reconfigurable sensor network architecture for distributed measurement systems,” in Proc. of the International Instrumentation and Measurement Technology Conference (I2MTC 2010), Austin, Texas, USA, 2010, pp. 198-203. Szilárd Jaskó, Tibor Dulai and Dániel Muhi, “Combined test model,” in Proc. of IeCCS 2007, AIP (American Institute of Physics) Conference Proceedings, 2007, pp. 406-409. Dániel Muhi and Tibor Dulai and Szilárd Jaskó, “Instant Messaging by SIP,” in Proc. of IeCCS 2007, AIP (American Institute of Physics) Conference Proceedings, 2007, pp. 414-416. Tibor Dulai, Szilárd Jaskó, Dániel Muhi. “Game Theory In Fleet Management,” in Proc. of IeCCS 2007, AIP (American Institute of Physics) Conference Proceedings, 2007, pp. 410-413. Szilárd Jaskó, Tibor Dulai, Dániel Muhi, Katalin Tarnay, “Process-based model for test system,” in Proc. of ISDA 2004, Budapest, 2004. pp. 507-511. Szilárd Jaskó, “A new mathematical formalism for the TTCN 3 core language,” in Proc. of CSCS 2004, Szeged, 2004, pp. 58.
12
Szilárd Jaskó, “Connection Between CSP and TTCN,” in Proc. of Information science & technology PhD school, 2004, pp. 31-33. [S15] Tibor Dulai, Szilárd Jaskó, Dániel Muhi, Dr. Katalin Tarnay, “New formal method in protocol development,” in Proc. of MicroCAD 2004, 2004, pp. 25-30. [S16] Szilárd Jaskó, Tibor Dulai, Dániel Muhi, Dr. Katalin Tarnay, “Generating Test Case(s) in CSP(Communicating Sequential Processes),” in Proc. of MicroCAD 2004, 2004, pp. 55-60. [S17] Szilárd Jaskó, “New views in the testing of protocols,” in Proc. of MicroCAD 2003, 2003, pp. 27-32. [S14]
Magyar konferencia kiadványában megjelent közlemények: Jaskó Szilárd, „Telekommunikációs rendszerek tesztelésének szabványai: ITU-T Z.140-142, ITU-T X.292-293,” Távközlési és Informatikai Hálózatok Szeminárium és Kiállítás Kiadványába 2004, Hajdúszoboszló, 2004, pp. 311-320. [S19] Jaskó Szilárd, „Szolgáltatás-felfedezés modellezése,” V. Országos Objektumorientált Konferencia Kiadványában, Dobogókő, 2002. pp. 31-32. [S20] Jaskó Szilárd, „Adatkommunikáció és modellezése,” Média-Informatika-Kommunikáció 2001 Kiadványában, Veszprém, 2001. pp. 117-119. [S18]
Kutatási jelentés: [S21]
Dr. Tarnay Katalin, Jaskó Szilárd és társaik. 2003. évi nagykanizsai nyári egyetem előadásainak összefoglalója, Informatikai és Hírközlési Minisztérium, 2003
13
Hivatkozások [H1] Recommendation Z.150, User Requirements Notation (URN) – Language Requirements and Framework, International Telecommunication Union, 2003. [H2] Recommendation Z.151, User Requirements Notation (URN) – Language definition, International Telecommunication Union, 2008. [H3] D. Amyot, “Introduction to the user requirements notation: learning by example,” Computer Networks: The International Journal of Computer and Telecommunications Networking , vol. 42, issue 3, pp. 285301 Jun. 2003. [H4] Z. Cai and E. Yu, “Addressing Performance Requirements Using a Goal and Scenario-Oriented Approach,” in Advanced Information Systems Engineering. Lecture Notes in Computer Science, vol. 2348, 2006, pp. 706-710. [H5] L. Liu and E. Yu, “Designing Web-Based Systems in Social Context: A Goal and Scenario Based Approach,” in Advanced Information Systems Engineering. Lecture Notes in Computer Science, vol. 2348, 2006, pp. 37-51. [H6] A. Pourshahid, T. Tran, “Modeling trust in e-commerce: an approach based on user requirements,” in Proc. of the ninth international conference on Electronic commerce (ICEC '07), Minneapolis, MN, USA, 2007, pp. 413-422. [H7] J. Hassine, J. Rilling and R. Dssouli, “Formal Verification of Use Case Maps with Real Time Extensions,” in SDL 2007: Design for Dependable Systems, Lecture Notes in Computer Science, 2007, pp. 225-241. [H8] J. Hassine, J. Rilling and R. Dssouli, “Timed Use Case Maps,” in System Analysis and Modeling: Language Profiles Lecture Notes in Computer Science, 2006, pp. 99-114. [H9] R. Matulevičius, P. Heymans and A. Opdahl, Comparing GRL and KAOS using the UEML Approach, Enterprise Interoperability II, Part I, Springer London, pp 77-88, 2007. [H10] S. Ghanavati, A. Siena, A. Perini, D. Amyot, L. Peyton, and A. Susi, “A Legal Perspective on Business: Modeling the Impact of Law,” in E-Technologies: Innovation in an Open World Lecture Notes in Business Information Processing, 2009, pp. 267-278. [H11] L. Liu and E. Yu, “Intentional Modeling to Support Identity Management,” in Conceptual Modeling – ER Lecture Notes in Computer Science, vol. 3288, 2004, pp. 555-566. [H12] G. Mussbacher, D. Amyot, “Extending the user requirements notation with aspect-oriented concepts,” in proc of SDL'09: Proceedings of the 14th international SDL conference on Design for motes and mobiles, 2009, pp. 115-132. [H13] A. Medve, “Advanced steps with standardized languages in the re-engineering process,” Computer Standards & Interfaces, vol. 30, issue 5, pp. 315-322, July 2008. [H14] J. Kealey, D. Amyot, “Enhanced use case map traversal semantics,” in proc of SDL'07: in Proc. of the 13th international SDL Forum conference on Design for dependable systems, 2007, pp. 133-149. [H15] J. Hassine, J. Rilling and R. Dssouli, “Abstract Operational Semantics for Use Case Maps,” Formal Techniques for Networked and Distributed Systems, Lecture Notes in Computer Science, vol. 3731, 2005, pp. 366-380. [H16] Y. He, D. Amyot and A. W. Williams, “Synthesizing SDL from Use Case Maps: An Experiment,” SDL 2003: System Design, Lecture Notes in Computer Science, vol. 2708, 2003, pp. 159. [H17] D. Amyot, J. Horkoff, D. Gross and G. Mussbacher, “A Lightweight GRL Profile for i* Modeling,” Advances in Conceptual Modeling - Challenging Perspectives Lecture Notes in Computer Science, vol. 5833, 2009, pp. 254-264. [H18] J. Roy, J. Kealey and D. Amyot, “Towards Integrated Tool Support for the User Requirements Notation,” System Analysis and Modeling: Language Profiles Lecture Notes in Computer Science, vol. 4320, 2006, pp. 198-215. [H19] C. Cares, X. Franch, A. Perini, A. Susi, “Towards interoperability of i* models using iStarML,”, Computer Standards & Interfaces, vol. 33, issue 1, pp. 69-79, Jan. 2011. [H20] M. R. Abid, D. Amyot, S. S. Somé and G. Mussbacher, “A UML Profile for Goal-Oriented Modeling,” SDL 2009: Design for Motes and Mobiles Lecture Notes in Computer Science, vol. 5719, 2009, pp. 133148.
14
[H21] D. Amyot, H. Farah and J. Roy, “Evaluation of Development Tools for Domain-Specific Modeling Languages,” System Analysis and Modeling: Language Profiles Lecture Notes in Computer Science, vol. 4320, 2006, pp. 183-197. [H22] D. Amyot, J. Roy and M. Weiss, “UCM-Driven Testing of Web Applications,” SDL 2005: Model Driven Lecture Notes in Computer Science, vol. 3530, 2005, pp. 1213-1229. [H23] D. Amyot, L. Logrippo, M. Weiss, “Generation of test purposes from Use Case Maps,” Computer Networks: The International Journal of Computer and Telecommunications Networking, vol. 49, issue 5, pp. 643-660, Dec. 2005. [H24] D. Amyot, S. Ghanavati, J. Horkoff, G. Mussbacher, L. Peyton, E. Yu, “Evaluating goal models within the goal-oriented requirement language,” International Journal of Intelligent Systems, Special Issue: Goal-driven Requirements Engineering, vol. 25, issue 8, pp. 841–877, Aug. 2010. [H25] Fesanghary, M., Khonsari, M. M, “On the Shape Optimization of Self-Adaptive Grooves,” Tribology Transactions, vol. 54, number 2, pp. 256-265, Mar. 2011. [H26] T. Chena, “A self-adaptive agent-based fuzzy-neural scheduling system for a wafer fabrication factory,” Expert Systems with Applications, vol. 38, pp. 7158-7168, Jun. 2011. [H27] X. Zhang, X. Jianga and P. J. Scotta, “Minimum zone evaluation of the form errors of quadric surfaces,” Precision Engineering, vol. 35, issue 2, pp. 383-389, Apr. 2011. [H28] Liu TCY, Luo L., Zhang L., “Self-adaptive effects of low intensity laser irradiation in prophylaxis of muscular fibrosis,” Lasers in surgery and medicine, vol. 43, pp. 975-975, Feb. 2011. [H29] Brusaferri A., Ballarino A., Carpanzano E., “Reconfigurable Knowledge-based Control Solutions for Responsive Manufacturing Systems,” Studies in informatics and control, vol. 20, issue 1, pp. 31-42, Mar. 2011. [H30] Wu GQ., Chen C., Yan XF., “Modified minimum covariance determinant estimator and its application to outlier detection of chemical process data,” Journal of applied statistics, vol. 38, issue 5, pp. 1007-1020, 2011. [H31] Sonmez OS., Dundar G., “Simulation-based analog and RF circuit synthesis using a modified evolutionary strategies algorithm,” Integration-the VLSI journal, vol. 44, issue 2, pp. 144-154, Mar. 2011. [H32] Wu LJ., Hu SD., Zhang B., Li ZJ., “Novel high-voltage power device based on self-adaptive interface charge,” Chinese physics, vol. 20, issue 2, Feb. 2011. [H33] Huang YP., Chang YT., Hsieh SL., Sandnes FE., “An adaptive knowledge evolution strategy for finding near-optimal solutions of specific problems,” Expert systems with applications, vol. 38, issue 4, pp. 38063818, Apr. 2011. [H34] Hermanto MW., Braatz RD., Chiu MS., “Integrated Batch-to-Batch and Nonlinear Model Predictive Control for Polymorphic Transformation in Pharmaceutical Crystallization,” Aiche Journal, vol. 57, issue 4, pp. 1008-1019, Apr. 2011. [H35] Yan L., Feng-Hong C., Xi S., Ming-Hui Z., Wen-Pin J., Dong-Gang C. and Hong M., “Self-Adaptive Resource Management for Large-Scale Shared Clusters,” Journal of Computer Science and Technology, vol. 25, number 5, pp. 945-957, Sep. 2010. [H36] C., Hui and Y., Shengxiang, “Improved performance of PSO with self-adaptive parameters for computing the optimal design of Water Supply Systems,” Engineering Applications of Artificial Intelligence, vol. 23, issue 5, pp. 727-735, Aug. 2010. [H37] Fan Y., Qing L. and Enhong C., “Benefit based cache data placement and update for mobile peer to peer networks,” Special Issue on Ubiquitous Media Technologies and Applications World Wide Web, vol. 14, number 3, pp. 243-259, May. 2011. [H38] Wei X., Ming X. and Yingwen C., “A Self-adaptive Fault-Tolerant Mechanism in Wireless Sensor Networks,” Scalable Information Systems, Lecture Notes of the Institute for Computer Sciences, vol. 18, 2009, pp. 228-240. [H39] Ting-peng L., “User interface design for decision support systems: A self-adaptive approach,” Information & Management, vol. 12, issue 4, pp. 181-193, Apr. 1987. [H40] P.R. Innocenta, “Towards self-adaptive interface systems,” International Journal of Man-Machine Studies, vol. 16, issue 3, pp. 287-299 Apr. 1982. [H41] Yves C., “Self-adaptive middleware: Supporting business process priorities and service level agreements,” Advanced Engineering Informatics, vol. 19, issue 3, pp. 199-211, July 2005.
15
[H42] Zhou Y., Ma X., Tao X. and Lu J., Wuhan “Towards a component framework for architecture-based selfadaptive applications,” University Journal of Natural Sciences, vol. 11, number 5, pp. 1227-1232. Sept. 2006. [H43] G. Rétvári, F. Németh, R. Chaparadza and R. Szabó, “OSPF for Implementing Self-adaptive Routing in Autonomic Networks: A Case Study,” Modeling Autonomic Communications Environments, Lecture Notes in Computer Science, Volume 5844/2009, 2009, pp. 72-85. [H44] Z. Harangozó and K. Tarnay, “FDTs in Self-adaptive Protocol Specification,” Self-Adaptive Software: Applications, Lecture Notes in Computer Science, vol. 2614/2003, 2003, pp. 105-118. [H45] G. Adamis and K. Tarnay, “Frame-Based Self-adaptive Test Case Selection,” Self-Adaptive Software: Applications, Lecture Notes in Computer Science, vol. 2614/2003, 2003, pp. 373-390. [H46] K. Tarnay, “Self-adaptive Protocols,” Self-Adaptive Software: Applications, Lecture Notes in Computer Science, vol. 2614/2003, 2003, pp. 213-218. [H47] Paraskevas A. Tsimoulas, G. I. Papadimitriou and Andreas S. Pomportsis, “A high-performance message prioritization and scheduling protocol for WDM star networks,” Photonic Network Communications, vol. 14, number 3, pp. 347-360, Dec. 2007. [H48] Smart-dust project, http://robotics.eecs.berkeley.edu/~pister/SmartDust/ [H49] Berkley WEBS, http://local.cs.berkeley.edu/webs/ [H50] CENS, http://research.cens.ucla.edu/ [H51] J. Kumagai, “Life of birds [wireless sensor network for bird study],” IEEE Spectrum, vol. 41, pp. 42–49, Apr. 2004. [H52] Zebra NET, http://www.princeton.edu/~mrm/zebranet.html [H53] Yute C., Jeng-Kuang H., “A Power-Line-Based Sensor Network for Proactive Electrical Fire Precaution and Early Discovery,” IEEE Transactions on Power Delivery, vol. 23 , issue 2, pp. 633 – 639, Apr. 2008. [H54] Yunseop K. E., R.G. Iversen, “Remote Sensing and Control of an Irrigation System Using a Distributed Wireless Sensor Network,” IEEE Transactions on Instrumentation and Measurement, vol. 57 , issue 7, pp. 1379 – 1387, July 2008. [H55] O. A. Postolache,.J. M. D. Pereira and P.M.B.S. Girao,. “Smart Sensors Network for Air Quality Monitoring Applications,” IEEE Transactions on Instrumentation and Measurement, vol. 58, pp. 3253– 3262, Sept. 2009. [H56] Chintalapudi, K. Fu, T. Paek, J. Kothari, N. Rangwala, S. Caffrey, J. Govindan, R. Johnson, E. Masri, S., “Monitoring civil structures with a wireless sensor network,” IEEE Internet Computing, vol. 10, issue 2, pp. 26 – 34, Mar.-Apr. 2006. [H57] Semertzidis, T. Dimitropoulos, K. Koutsia, A. Grammalidis, N., “Video sensor network for real-time traffic monitoring and surveillance,” Intelligent Transport Systems, vol. 4, issue 2, pp. 103 – 112, Jun. 2010. [H58] Hao J. L., Chen J. W., Siyue C. L., H., “A Reliable and High-Bandwidth Multihop Wireless Sensor Network for Mine Tunnel Monitoring,“ IEEE Sensors Journal, vol. 9, issue 11, pp. 1511 – 1517, Nov. 2009. [H59] D. Malan, T. Fulford-Jones, M. Welsh, S. Moulton, “CodeBlue: An Ad Hoc Sensor Network Infrastructure for Emergency Medical Care,” in Proc. of Workshop on Applications of Mobile Embedded Systems (WAMES 2004), 2004. [H60] Jang, I.-H. Yeom, H.-G. Sim, K.-B., “Ring sensor and heart rate monitoring system for sensor network applications,” Electronics Letters, vol. 44, issue 24, pp. 1393 – 1394, Nov. 2008. [H61] Shu-Di Bao Poon, C.C.Y. Yuan-Ting Zhang Lian-Feng Shen, “Using the Timing Information of Heartbeats as an Entity Identifier to Secure Body Sensor Network,” IEEE Transactions on Information Technology in Biomedicine, vol. 12, issue 6, pp. 772 – 779, Nov. 2008. [H62] Ghasemzadeh, H. Jafari, R. Prabhakaran, “A Body Sensor Network With Electromyogram and Inertial Sensors: Multimodal Interpretation of Muscular Activities,” IEEE Transactions on Information Technology in Biomedicine, vol. 14, issue 2, pp. 198 – 206, Mar. 2010. [H63] Guangming S. Z., Wei W., Zhang A. S., “A Hybrid Sensor Network System for Home Monitoring Applications,” IEEE Transactions on Consumer Electronics, vol. 53, issue 4, pp. 1434 – 1439, Nov. 2007. [H64] Simon, G., Maróti, M., Lédeczi, A., Balogh, G., Kusy, B., Nádas, A., Pap, G., Sallai, J., Frampton, K., “Sensor Network-Based Countersniper System,” In Proc of the Second ACM Conference on Embedded Networked Sensor Systems (SenSys), Baltimore, MD, USA, Nov. 2004, pp.1-12.
16
[H65] Ledeczi A., Nadas A., Volgyesi P., Balogh G., Kusy B., Sallai J., Pap G., Dora S., Molnar, K., Maroti M., Simon G., "Countersniper System for Urban Warfare," ACM Transactions on Sensor Networks, Vol. 1, No. 2, pp. 153-177, Nov. 2005. [H66] A. Arora and P. Dutta and S. Bapat and V. Kulathumani and H. Zhang and V. Naik and V. Mittal and H. Cao and M. Demirbas and M. Gouda and Y. Choi and T. Herman and S. Kulkarni and U. Arumugam and M. Nesterenko and A. Vora and M. Miyashita, “A Line in the Sand: A Wireless Sensor Network for Target Detection, Classification, and Tracking,” Computer Networks, vol.46, pp. 605-634, 2004. [H67] Gao, R.X. Zhaoyan Fan, “Architectural design of a sensory node controller for optimized energy utilization in sensor networks,” IEEE Transactions on Instrumentation and Measurement, vol. 55, issue 2, pp. 415 – 428, Apr. 2006. [H68] Mondinelli, F. Kovacs-Vajna, Z.M., “Self-localizing sensor network architectures,” IEEE Transactions on Instrumentation and Measurement, vol. 53, issue 2, pp. 277 – 283, Apr. 2004. [H69] J. Hill, R. Szewczyk, A. Woo, S. Hollar, D. Culler and K. Pister, “System architecture directions for networked sensors,” in Architectural support for programming languages and operation systems, 2000, pp. 93-104. [H70] Jianyong Lin Wendong Xiao Lewis, F.L. Lihua Xie, “Energy-Efficient Distributed Adaptive Multisensor Scheduling for Target Tracking in Wireless Sensor Networks,” IEEE Transactions on Instrumentation and Measurement, vol. 58, issue 6, pp. 1886 – 1896, Jun. 2009. [H71] Bertocco, M. Gamba, G. Sona, A. Vitturi, “Experimental Characterization of Wireless Sensor Networks for Industrial Applications,” IEEE Transactions on Instrumentation and Measurement, vol. 57 , issue 8, pp. 1537 – 1546, Jul. 2008. [H72] Moustapha, A.I. Selmic, R.R., “Wireless Sensor Network Modeling Using Modified Recurrent Neural Networks: Application to Fault Detection,” IEEE Transactions on Instrumentation and Measurement, vol. 57, issue 5, pp. 981 – 988, May 2008. [H73] G. Vakulya, G. Simon, „Adaptive Acoustic Localization Algorithm”, in Proc. 2010 International Instrumentation and Measurement Technology Conference, Austin, TX, May 3-6, 2010, pp. 405-411. [H74] P. Levis and D. Culler, “Maté: a tiny virtual machine for sensor networks,” in Proc. of the ACM Conference on Architectural Support for Programming Languages and Operating Systems, New York, NY, USA, 2002, pp. 85-95. [H75] P. Levis, D. Gay, and D. E. Culler, “Active Sensor Networks,” in Proc. of NSDI'05: Second Symposium on Networked Systems Design and Implementation, USENIX Association Berkeley, CA, USA, 2005., pp. 343-356. [H76] A. Boulisa, C. Hanb, R. Sheab, M. B. Srivastava, “SensorWare: Programming sensor networks beyond code update and querying,” Pervasive and Mobile Computing, vol. 3, pp. 386–412, Aug. 2007. [H77] J. Koshy , I. Wirjawan, R. Pandey, Y. Ramin, “Balancing computation and communication costs: The case for hybrid execution in sensor networks,” Ad Hoc Networks, vol. 6, pp. 1185–1200, Nov. 2008. [H78] D. Gay, P. Leves, R. V. Behren, M. Welsh, E. Brewer and D. Culler, “ The nesC Language: A Holistic Approach to Networked Embedded Systems,” in Proc. of Conference on Programming Language Design and Implementation PLDI, New York, NY, USA, 2003, pp. 1-11. [H79] C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, NJ, 1985. [H80] He J. and C. A. R. Hoare. “Algebraic specification and proof of a distributed recovery algorithm,” Distributed Computing, vol. 2, pp. 1–12, 1987. [H81] Peleska, J., “Applied formal methods - from csp to executable hybrid specifications,” in Communicating Sequential Processes. Lecture Notes in Computer Science LNCS, vol. 3525, 2005, pp. 293–320. [H82] Evans, N. and Treharne, H., “Interactive tool support for CSP || B consistency checking,” Formal Aspects of Computing, vol. 19, issue 3, pp. 277-302, 2007. [H83] D. Gift Samuel, M. Roggenbach, and Yoshinao I., “The Stable Revivals Model in CSP-Prover,” Electron. Notes Theor. Comput. Sci., vol. 250, 2 pp. 119-134, Sep. 2009. [H84] L. O'Reilly, M. Roggenbach, and Yoshinao I., “CSP-CASL-Prover: A Generic Tool for Process and Data Refinement,” Electron. Notes Theor. Comput. Sci., vol. 250, 2, pp. 69-84, Sep. 2009. [H85] M. G. Hincheya, J. L. Rasha, C. A. Rouffb, “Denis Gracanin. Achieving dependability in sensor networks through automated requirements-based programming,” Computer Communications, vol. 29, pp. 246–256, 2006. [H86] A. Mota and A. Sampaio,.”Model-checking CSP-Z: strategy, tool support and industrial application,” Sci. Comput. Program., vol. 40, 1, pp. 59-96, May. 2001.
17
[H87] M. Roggenbach, “CSP-CASL: a new integration of process algebra and algebraic specification,” Theor. Comput. Sci., vol. 354, 1, pp. 42-71, Mar. 2006. [H88] C. Fischer, “CSP-OZ: a combination of object-Z and CSP,” in Proc. of the IFIP TC6 WG6.1 international workshop on Formal methods for open object-based distributed systems (FMOODS '97), 1997, pp. 423-438. [H89] Evans, N. and Treharne, H., “Interactive tool support for CSP || B consistency checking,” Formal Aspects of Computing, vol. 19, issue 3, pp. 277-302, 2007. [H90] Isobe, Y. and Roggenbach, M., “A Complete Axiomatic Semantics for the CSP Stable-Failures Model,” CONCUR 2006 – Concurrency Theory Lecture Notes in Computer Science, vol. 4137, 2006, pp. 158-172. [H91] P. G. O'Donoghue, M. E. C. Hull, “Using timed CSP during object oriented design of real-time systems,” Information and Software Technology, vol. 38, issue 2, pp. 89-102, 1996. [H92] J. Ouaknine, S. Schneider, “Timed CSP: A Retrospective,” Electronic Notes in Theoretical Computer Science Proc. of the Workshop "Essays on Algebraic Process Calculi" (APC 25), vol. 162, 2006, pp. 273276. [H93] J. Ouaknine and J. Worrell, “Timed CSP = closed timed e-automata,” Nordic J. of Computing, vol. 10, 2 pp. 99-133,May. 2003. [H94] L. M. Patnaik, B. R. Badrinath, “Implementation of CSP-S for description of distributed algorithms,” Computer Languages, vol. 9, issues 3-4, pp. 193-202, 1984.
18
