Programozás | UML » Roel Wieringa - Az UML formalizálása rendszertechnikai megközelítésben

Az UML formalizálása rendszertechnikai megközelítésben Roel Wieringa roelw@cs.utwentenl Kivonat Ez az elemzés megtárgyalja bármely félformális jelölésrendszer formalizációjának beágyazódását egy módszertanba. Bemutatunk egy módszertani keretrendszert a rendszertechnikán alapuló szoftverspecifikációra és megmutatjuk, hogyan lehet az UML-t ebbe a keretrendszerbe illeszteni. Majd, az UML formalizálásának egy lényeges modellközelítését tárgyaljuk ezen keretrendszeren belül. Végül, az UML átmenetrendszerének szemantikáját tárgyaljuk, amely illeszkedik ezen szemantikai közelítéshez. A formális részleteket nem adjuk meg, de hivatkozásokat adunk olyan helyekre, ahol ezek fellelhetőek. 1. Formalizmus és Módszer Néhány kutatócsoport jelenlegi kutatása grafikus specifikációs technikák formalizálására irányul [5,9,20,37]. Közeli kapcsolat van egyrészt a rendszer specifikációk jelölésrendszerének választott szemantikája és

másfelöl a rendszer specifikációk választott módszere között. Például, ha a módszer megkülönböztet egy specifikációs szintet egy implementációs (programnyelv) szinttől, mint a Syntropy-ban [6], akkor az összetett objektumok választott szemantikája az implementációs szinten megérthető programnyelvi konstrukciókkal kifejezve, de a specifikációs szinten értelmeznünk kell, hogy az összetétel (kompozíció) mit jelent a rendszer tárgy tartományában. Ez azt jelenti, hogy az összetétel szintaktikus szerkezetének jelentését különbözően kell formalizálnunk ezen a két specifikációs szinten. Általánosítsuk ezt az észrevételt: függ a fejlesztési módszer informális irányvonalától és filozofiájától az, hogy hogyan kell formalizálnunk az informális jelölésrendszert, és egy jelölés különböző formális szemantikát adna különböző módszertani cél esetén. Ez azt is jelenti, hogy egy jelölés bármely használatát, még

ha annak szemantikája formalizált is, kísérnie kell választott használatának informális leírása (pl. mint egy magasszintű specifikáció modellje vagy mint egy részletes implementáció modellje). Ellenben, ha egyszer formalizálunk egy jelölést egy meghatározott célra, akkor annak használatához ezen formalizációból nyerhetünk informális irányvonalat. A formális szemantika mindig kifejezhető informális kifejezésekkel. 1 Például, Gunter Saake-kal együtt formalizáltuk a Shlaer-Mellor módszer részeit és megmutattuk, hogy a formalizáció segítségével hogyan tehető a módszer precízebbé és kevésbé redundánssá ebben a reprezentációs technikában [40]. Másik példa, amikor azért használjuk az objektum-orientált fogalmi modell formalizálását, hogy néhány informális, egyszerű és egyértelmű irányvonalat nyerjünk fogalmi adatbázis modellek [32] felépítéséhez. A módszer használóinak és jelöléseinek nem kell tudniuk a

formális szemantika matematikai hátteréről, de a formális szemantikának köszönhetően a jelölések használata egyszerűbb, egyértelműen tudunk levezetni és világos a „használat iránya”. Így mikor elkezdjük a formalizálást egy jelölés meghatározott használatának módszertani elemzéséből, akkor a formalizációval leegyszerűsíthetjük és javíthatjuk a módszert és annak informális irányvonalát. 1 Egy hasznos (useful) formalizációmindig kifejezhető informális kifejezésekkel. Ebben a rövid cikkben adunk egy módszertani keretrendszert az objektum-orientált szoftver rendszerek UML-szerű jelöléseinek formalizálására. Megmutatjuk, hogyan kell alkalmazni a keretrendszert az UML-hez, majd megtárgyaljuk ennek következményeit az UML formalizált szemantikájára nézve. Ezt a megközelítést követő formalizációra példa máshol található [37]. 2. A TRADE keretrendszer Az itt bemutatásra kerülő keretrendszer ipari

terméktechnikai [29] és rendszertechnikai [11,12] keretrendszerek elemzésén alapul. Alkalmazzák követelmény technikai módszerekhez [34] és integrált formális/félformális követelmény specifikációhoz [38]. A keret felső szintjén bármely rendszerfejlesztésben (szoftver vagy nem szoftver) négy dimenziót tudunk azonosítani. Ezek a dimenziók ortogonálisak (merőlegesek) egymásra abban az értelemben, hogy a technikák és a módszerek kiválasztása mindegyikben nagymértékben független egymástól. - Idő: Az időbeli dimenzió tartalmazza a fejlesztési folyamat tervezési döntéseinek időbeli sorozatát. Tervezési döntések egy eltervezett sorozatát fejlesztési stratégiának nevezzük A lehetséges opciók: lineáris fejlesztési folyamat, növekedési fejlesztési folyamat, fejlődési fejlesztési folyamat stb. végrehajtása Ezek különböznek a tervezési döntések időbeli rendezésében és az általuk engedélyezett visszalépésekben.

Például, lineáris fejlesztésben először meghozzuk az összes követelmény döntést, majd a szerkezeti tervezési döntéseket, végül a részletes tervezési és implementációs döntéseket, mindezt visszalépés lehetősége nélkül. Növekedési fejlesztésben a részletes tervezés és implementáció iteratívan készül, de a szerkezet nem javítható, ha már egyszer meghatároztuk. Fejlődési fejlesztésben visszalépés engedélyezett a szerkezetre, sőt, akár még a követelmény döntésekre is. Ezek az implementációk során szerzett tapasztalatok alapján javíthatók. Azért emeltük ki ezt a dimenziót, mert a fejlesztési stratégia kiválasztása független más dimenzióbeli választástól. Gyakorlatilag független strukturált vagy objektum-orientált technika választásától. - Logika: Ezt indoklási (justification) dimenziónak is nevezhetjük. Minden tervezési döntést meg kell indokolni, és a legjobb mód erre, hogy ésszerűen átalakítjuk,

mintha az ésszerű döntési ciklus szerint csináltuk volna: - Elemzés (problémáknak, szükségleteknek, céloknak stb.) - Szintézis, összeillesztés (lehetséges megoldásoknak, azaz lehetséges terveknek). Ezen a helyen a specifikáció és a leíró technikák hasznosak. - Becslése az alternatív megoldások implementálási következményeinek. Ez a történések megfigyelésétől terjedhet azokig, akik azonos körülmények között implementálták ezt a megoldást, a prototípus készítésén, szimuláció végrehajtásán, terv jellemzőinek formális indoklásán stb keresztül. - Kiértékelése a megbecsült következményeknek. Ez elhanyagolt szempont a szoftver készítésben, de más termékkészítési ágazatban sok mennyiségi és minőségi technika használatos. - Kiválasztása egy megoldásnak. 2 Az ésszerű átalakítás hasonló, mint amit Parnas és Clements [24] egy ésszerű folyamat feltekercselésének nevez. Tudománytörténeti kutatások

megmutatják, hogy ez egy jelentős technika, amit más tudományokban használnak [19]. A kiszámítás gyakran szabálytalan folyamata (mely fogalmak írnak le legjobban egy tartományt, hogy kell ezeket definiálni és mérni, és milyen a tapasztalati eredmények és elemzés szerkezete) le van írva könyvekben ésszerű argumentumok segítségével, melyek alternatívákat hasonlítanak össze kritériumok segítségével, melyek úgy vannak leírva, mintha előre meg lettek volna becsülve. Kuhn a racionalizálás és a fogalmi struktúrák egyszerűsítésének folyamatát a matematikában és a tapasztalati tudományban „mopping up”-nak, azaz „tisztogatás”-nak nevezi [18]. Ez a szokásos tudomány része. Ellentétben Parnas és Clements „tekercselés” kifejezésének használatával ez nem megtévesztés: a lehetőség egy folyamat átalakítására (mintha az követne egy ésszerű döntési ciklust) képezi a folyamat eredményének indoklását. - Szempont:

Egy rendszer szempontja a rendszer jellemzőinek egy részhalmaza. Rendszerint, egy szempont a szaktudás sajátos területe által definiált. A fejlesztést érintik mechanikai, elektronikai vagy szoftver szempontok, társadalmi, törvényi vagy pénzügyi szempontok, kereskedelmi szempont stb. Sikeres rendszerfejlesztésben a fontos szempontokat integrált módon kezelik. Szociáltechnikai módszerek megpróbálják integrálni a rendszerfejlesztés társadalmi és technikai szempontjait. Együttműködő tervezésben különböző területek szakemberei (kezdve a tervezéstől a marketing és vásárló támogatásig) együtt dolgoznak egyetlen integrált tervezési projektben [27]. - Aggregációs szint: A rendszerek aggregációs hierarchiákba szerveződhetnek, és a fejlesztési stratégiától függetlenül alrendszer, al-alrendszer stb hierarchiájaként kell megadni és felépíteni. Ez történhet alulról-felfelé, felülről-lefelé, belülről-kifelé vagy teljesen

összevissza, de a folyamat végeredményéül kapott rendszernek alrendszerek hierarchiájából kell állnia. Formális specifikáció, ahogy azt a szoftverkészítésben ismerjük, csak azokban a készítési feladatokban játszik szerepet, ahol hasznos, ha egy formális szintaxist, matematikai szemantikát és műveleti szabályokat használó nyelven írunk egy leírást, amelyek eléggé explicitek, hogy beprogramozhassuk őket a számítógépbe. Ha megnézzük az ésszerű tervezési ciklust, a következőket vehetjük észre: - Elemzés közben hasznos lehet a probléma tartomány (részeinek) formális leírása. - Szintézis közben egy vagy több lehetséges tervet lehet formálisan megadni. - Becslés közben egy formálisan megadott terv jellemzőit lehet formálisan származtatni. Ez nem jelenti azt, hogy minden esetben hasznos vagy megéri ilyet csinálni. Tapasztalati tanulmányok mutatják, hogy egy formális specifikáció hasznos lehet jólstruktúrált és stabil

tartományokban, ahol a megtervezett terméknek biztonságosnak kell lennie [1,7]. Most megnöveljük a dimenziók számát a keretrendszerben, amely kizárólag a specifikációs technikákra vonatkozik(formális és informális egyaránt). Struktúrált és objektum-orientált specifikációs módszerek alapos elemzése kimutatja, hogy három szempont van, melyekre ezek a módszerek specifikációs technikákat kínálnak [35]: 3 - Függvények: Ez egy túlterhelt kifejezés, szoftvertervezésben egy programozási nyelven megírt rutinokkal van összefüggésben. Itt általánosabb értelemben használjuk, mely minden más szoftvertervezési ágban használatos: egy termék függvénye egy termék külső kölcsönhatásának hasznos része. Hasznos egy külső actornak, aki alkalmazza a függvényt a termékkel való kölcsönhatásban, vagy aki másokat kényszerít rá, hogy kölcsönhatásba lépjenek a termékkel. Ez nagyon közel van ahhoz, amit use cases-nek hívunk az

UML-ben vagy szolgáltatásoknak telekommunikációs rendszertervezéskor. Egy termék függvénye egy szolgáltatás, melyet a termék felkínál a környezetének. A függvények nem a rendszer komponensei (noha tudunk olyan komponenseket megadni, hogy megfeleljenek függvényeknek). A függvényspecifikációk különféle módszerei által felkínált technikák tartalmaznak esemény-válasz párokat (struktúrált elemzés), elő- és utófeltételes specifikációkat (formális technikák, mint Z, VDM vagy dinamikus logika) és use cases leírásokat (UML). - Viselkedés: függvények időbeli sorozata. Viselkedés specifikációkhoz felkínált technikák állapotátmenet diagramok nagy választékát (Moore, Mealy, állapotgrafikonok, SDL állapotgépek) és néhány temporális és valósidejű logikát tartalmaznak biztonságossági és elevenségi jellemzők specifikálásához. Ide soroljuk még az invariánsokat specifikáló technikákat is, azaz olyan jellemzők, melyek

egy viselkedés minden lehetséges állapotában megmaradnak. - Kommunikáció: függvények sorozata a „tér”-ben. Kevésbé képletesen, leírja, hogy a termék hogyan kapcsolódik a környezetében lévő entitásokhoz és hogyan lép kölcsönhatásba azokkal az entitásokkal. Ez a szempont struktúrált és objektum-orientált módszerekben nagyon felületesen van leírva. SDL sokkal gondosabb ebből a szempontból és a folyamatalgebrák nagyon nagyon gondosak ebből a szempontból. Ez a három szempont felbukkan az aggregációs hierarchia minden szintjén. A felső szinten a viselkedést rendszerint események és válaszok előfordulására vonatkozó megszorításokkal írják le. Az alacsonyabb aggregációs szinteken használhatunk állapotátmenet diagramokat a viselkedés konstruktívabb specifikálásához. Ezzel a keretrendszerrel egy specifikációs technikai eszköztárat adtunk meg, melyet a struktúrált és objektum-orientált módszerektől kölcsönöztük,

és TRADE-nek (Toolkit for Requirements and Design Engineering) [36]2 nevezzük. Ez nem egy szoftver eszköztár, hanem céleszközök gyűjteménye, azaz fogalmak, reprezentációs technikák és ezen technikák használatára vonatkozó irányvonalak.3 A TRADE elég általános ahhoz, hogy bármely olyan formális specifikációs nyelvvel kombinálhassuk, mely képes beszélni eseményekről és válaszokról (azaz külső rendszerfüggvényekről) és logikai adatszerkezetekről. Alkalmazták egy ipari eset tanulmányában kombinálva az Albert II specifikációs nyelvvel, mely temporális logikán [4,38] alapul. Dinamikus logikával kombinálva alkalmazták egy ipari terméksejt [33] specifikálásához is. Most tekintsük a TRADE keretrendszeren belül az UML részeinek formalizálását [37]. A következő részben ennek a formalizációnak a megközelítését tárgyaljuk. 2 3 A TRADE másik neve NYAM (Not Yet Another Method). Ezen céleszközök használatához szoftver

támogatás [8]-ban található. 4 3. Az UML leképezése TRADE-re Az UML formalizálásához először a célt kell meghatároznunk, amire az UML-t használni akarjuk. Ezen cikk megközelítésében ez azt jelenti, hogy el kell helyeznünk az UML-t a TRADE keretrendszerben. Mivel a TRADE keretrendszer alkalmazható a rendszer aggregációs hierarchiájának minden szintjén, pontosabban meg kell adnunk, hogy hol alkalmazzuk a hierarchiában az UML-t. Az alkalmazhatóság hierarchiáját felülről-lefelé nagyjából a következőképpen írhatjuk le: - Szervezet - Szervezeti egységek - Számítógép alapú rendszerek (magába foglalja a hardvert és a szoftvert) - Szoftverrendszerek - Szoftver alrendszerek - Szoftver objektumok - Ütemezhető szekvenciális feladatok Ez nem valami nehéz és gyors rétegezés. Különböző módszerek különböző aggregációs szinteket azonosítanak. Pontosabban, különböző alkalmazásokat modellezhetünk különböző aggregációs

hierarchiák használatával. Nincs általános rétegződés, amely alkalmazható lenne minden lehetséges alkalmazásra. Megfigyelhető, hogy objektum-orientált szoftver fejlesztési módszerek figyelmen kívül hagyják az alrendszer szintet. Az egyetlen kivétel az Octopus [2] A strukturált táborban Schumate és Keller [31], illetve Gomaa [10] ad hasznos alrendszer strukturálási kritériumokat. Objektum-orientált szerkezetek kutatása eltolódik manapság a hierarchia alacsonyabb szintjei felé. Az UML specifikációs technikák gyűjteménye, melyeket szoftverspecifikációra szánnak. Az egyetlen kivétel a tevékenység diagramok, melyek célja különféle üzleti modellezések (munkafolyam folyamatok) és módszer implementációk vezérlő szerkezeteinek feltérképezése. Az első ábra egy lehetséges nézet arra, hogyan tudjuk a főbb technikákat leképezni a TRADE specifikációs keretrendszerre. Use case diagram Külső függvények X Dekompozíció Függvény

Viselkedés Kommunikáció Osztály diagram Állapotgrafikon Szekvenciális (Statecharts) diagram Együttműködés i diagram X X X X X X X 1.ábra: Technikák az UML-ben 1. objektum . m. objektum 1. függvény X . n. függvény X X X 2.ábra: Nyomonkövetési táblázat 5 Más nézet is lehetséges, pl. szekvenciális diagramok használata a use cases bemutatására Az 1.ábra nézete az, amit formalizálni akarunk A táblázat feltételez egy szoftver (al)rendszer nézetet, mint szoftver objektumok gyűjteményét, melyek felülete bemutatható osztály diagramon. Az objektum felületek tartalmaznak műveleteket, melyeket végrehajthatunk és jeleket, melyeket küldhetünk és fogadhatunk. A lejjebb tárgyalt formalizációban az attribútumok is az objektum felület részei. Ezt megindokoljuk a következő részben Először tekintsük a tevékenység diagramok és az implementációs diagramok keretrendszerbe helyezésének módját. Ehhez nézzük meg az

aggregációs hierarchia két szomszédos szintje közötti kapcsolatot. Ez kifejezhető a rendszertervezésből ismert nyomonkövetési táblázattal. A 2ábra vízszintesen mutatja a rendszerfüggvényeket, és függőlegesen az egyes objektumokat. A táblázat minden bejegyzése egy objektum felületet mutat (egy művelet vagy jel vagy egy attribútum, az itteni formalizálásban). Ezt lehet egy objektum függvényének is nevezni Ezért minden egyes sor minden olyan műveletet mutat, amely az objektum viselkedésében előfordul, és minden egyes oszlop azt mutatja, hogy kommunikálnak az objektumok egy rendszerfüggvény megvalósításához. A táblázat így összegzi a specifikációs keretrendszerünk három szempontját, úgymint függvények, viselkedés és kommunikáció. A táblázat az egyes objektumokat mutatja. Mivel a szoftverobjektumok száma dinamikusan változhat a szoftver végrehajtása során, hasznosabb függőlegesen az objektumosztályokat feltüntetni és

hagyjuk a bejegyzéseket az osztályok ismeretlen példányainak felületei számára. A tevékenység diagramok a viselkedést mutatják, amint az „átfolyik” az objektumok gyűjteményén keresztül. Úgy is nézhető, mint egy viselkedési reprezentációja annak, hogy mi történik egy oszlopban. Ha egy rendszerfüggvény tartalmaz egy eseményt és egy választ, akkor egy tevékenység diagram segítségével megnézhetjük, hogy mi történik a folyamatban az eseménytől a válaszig. Alternatívan az együttműködési vagy szekvenciális diagramok is azt mutatják, mi történik ebben a folyamatban. Végül az implementációs diagramok azt mutatják, hogyan vannak a szoftver komponensek hozzárendelve a fizikai erőforrásokhoz egy hálózatban és ezért megadja a nyomonkövethetőségi információt, amelyek két aggregációs hierachiát kötnek össze, szoftver aggregációs hierarchiát, melyet itt érintettünk, és a hardver aggregációs hierarchiát, melyben a

fizikai erőforrások léteznek. 4. Az elsőrendű dekompozíciós szint Mielőtt az UML formalizálásának saját megközelítését tárgyalnánk, be kell mutatnunk a különbséget a kétfajta szoftverrendszer dekompozíció között. Egy elsőrendű dekompozíció egy felbontás komponensekre (esetünkben objektumok), melyet teljesen a szoftver külső környezetére való hivatkozás motivál. Néhány példa dekompozíciós kritériumokra: - Funkcionális dekompozíció: a komponensek megegyeznek a külső függvényekkel. - Subject-domain orientált dekompozíció: a komponensek megegyeznek a subject domain objektumokkal. - Esemény felosztás: a komponensek megegyeznek a rendszer esemény-válasz párjaival. - Eszköz felosztás: a komponensek megegyeznek az eszközökkel, amelyekkel a rendszernek kommunikálnia kell. 6 Más kritériumok is lehetségesek. A JSD egy olyan módszer, ami subject-domain orientált dekompozíciót használ a dekompozíció stabil részeinek

azonosítására, és funkcionális dekompozíciót a funkcionális komponensek azonosítására, melyek jelentése a subject-domain orientált rész kifejezéseiben definiált [17]. Az elsőrendű dekompozíciót elsőrendű modellnek nevezzük McMenamin és Palmer [22] alapján, és ez összhangban van a Syntropy [6] specifikációs modelljével. Mivel nem veszi figyelembe az implementációs határokat, megmutat egy implementációt egy tökéletes technológián. Így nem jelenik meg semmilyen implementációs hiba, minden komponensnek határtalan számítási kapacitás és memóriahely áll rendelkezésére stb. Így az elsőrendű dekompozícióban egy objektum attribútumai nem példányváltozók, amik az implementáció részei, és el kell rejteni az objektum klienseitől. Ezzel szemben az elsőrendű szinten az attribútumok tárolják az objektum megfigyelhető állapotának egy részét és láthatóak az objektum kliensei számára. Így az elsőrendű attribútumok az

objektum felületének részei Egy implementációs dekompozíció azon dekompozíciók, melyek figyelembe veszik az implementációs platform alapjául szolgáló szempontokat. Itt megjelennek a hibák, a műveletek bizonyos idő alatt hajtódnak végre stb. Ez összhangban van a Syntropy implementációs modelljével. Megjegyezzük, hogy egy elsőrendű dekompozíció figyelembe veszi a külső entitások minden határát és a felületben lévő entitások határait, melyeket azon entitások jellemzői kényszerítettek ki. Megadjuk egy elsőrendű dekompozíció néhány előnyét: - Az elsőrendű dekompozíció határt szab a tervezői szabadságnak. Világosan leírja, hogy a világ mely részéről dönthet a tervező (a rendszer belseje) és mely részeket kell elfogadni, ahogy van (külső környezet). Ez tartalmazza a természetes és előzőleg telepített rendszereket [25] és a tervezőnek foglalkoznia kell a külső környezet minden határával. - Az elsőrendű

dekompozíció megengedi, hogy követelményeket explicit módon készítsünk az implementáción. Egy elsőrendű dekompozíció tervezése rendszerint kitűnő módja a kívánt külső jellemzők specifikációja rejtett szempontjainak feltárására. Gyakran előfordul, hogy nem tudjuk a külső jellemzők specifikációját explicitebben elkészíteni a rendszer belső összetételére vonatkozó feltevés nélkül. Egy elsőrendű dekompozíció segítségével a külső jellemzőket explicitebben készíthetjük el implementációs megfontolások bevezetése nélkül. - Az elsőrendű dekompozíció mint közvetítő lép fel a kívánt külső rendszerjellemzők specifikációja (kívánt esemény/válasz viselkedése, kívánt viselkedésjellemzők) és a lehetséges implementáció között. Mivel ez független az aktuális implementációtól, invariáns marad minden lehetséges implementációban. Ez egy fontos eszközt jelent a követelmények és a különböző

implementációk közötti nyomonkövethetőség fenntartásában. - Mivel egy elsőrendű dekompozíciót a külső környezet kifejezései motiválják, ez egy fontos eszköz a tervezés alapjának fenntartásában. Ez ad elsősorban indokokat (külső követelményekben gyökerezik) bizonyos implementációs választásokhoz, melyet minden lehetséges implementációban így kell elkészíteni. A következő részben a szemantikát tárgyaljuk, melyet az UML-nek tartalmaznia kell, mikor egy elsőrendű dekompozíció megvalósításához használjuk. 7 5. Az átmenetrendszer szemantikájának vázlata az UML-hez Az elsőrendű dekmpozíció bemutatásához használt UML (formális vagy informális) szemantikának a következő dolgokat kell tudnia: - Meg kell adnia a szemantikát az objektumok és az osztályok alapvető fogalmaihoz. - Gondoskodnia kell azon szemantikus struktúrákról, amelyek az objektum függvényeit, viselkedését és kommunikációját mutatják be. -

Meg kell mutatnia, hogy objektumok egy halmaza hogyan tudja megvalósítani egy rendszer függvényeit, viselkedését és kommunikációját. Az elsőrendű szinten egy objektumot egy azonosítóval jelölhetünk, mely egyedi az összes osztály összes lehetséges objektumára. Az attribútumokat jelölhetjük egyváltozós módosítható függvényekkel, melyek argumentumként egy objektumazonosítót kapnak és egy értéket vagy egy objektum azonosítót ad át eredményként. Mivel az attribútumoknak sok lehetséges értékük van, ezek definiálják az objektum összes lehetséges állapotának halmazát. A műveletek módosítják az attribútumokat, és ezen állapotok közötti átmenetekként ábrázolhatóak, így megadják az átmenetrendszer szerkezetét. Objektumok egy halmazára, minden állapot objektum azonosítók egy halmazát tartalmazza, a megadott attribútumértékekkel. Egy rendszer minden lehetséges állapotára teljesülniük kell az invariánsoknak. A

legfontosabb megszorításokat leszámítva az invariánsok nem igazán részei az UML-nek. Az átmenetek hozzátehetnek azonosítókat a halmazhoz vagy törölhetnek azonosítókat a halmazból és megváltoztathatják a halmazban lévő objektumok attribútumainak értékét, és gondoskodva az invariánsokkal való kapcsolatról. Egy objektumosztály értelmezhető kiterjedten mint (azonosítók) összes lehetséges példányainak halmaza, és az elsőrendű szinten az osztályozás egyszerűen halmaz beleértve az osztálykiterjesztéseket. Korábban már bemuttatuk ennek egy formalizációját, amely pótlólag foglalkozik az osztályváltás lehetőségével [39]. Ebben a formalizációban különbség van a fix osztálytagság (ami az objektum azonosítójának része) és a dinamikus osztálytagság között. Például, egy személy a SZEMÉLY osztály fix tagja, mivel ez a tagság a személy létezése során nem változik. Létezése során beléphet az IDŐS SZEMÉLY

osztályba, amely dinamikus osztálytagság. Ebbe az osztályba való belépés a személy azonosítását nem változtatja meg Ráadásul, különbség van az objektumosztályok és a szereposztályok között. Egy szerep hasonlít az objektumra abban, hogy saját azonossága van. A különbség abban áll, hogy egy szerepet másik szerepnek vagy objektumnak kell játszania. Ez megmutatja a szerep létezésének függőségét annak eljátszójától. Például, egy alkalmazott modellezhető úgy, mint a személy egy szerepe. A formalizáció definiálja a order-sorted (sorbarendezett) dinamikus logika egy verzióját is, amit DOL-nak (Dinamikus Objektum Logika) nevezünk, ami engedélyezi nekünk, hogy megadjuk ezeket a szemantikus struktúrákat a dinamikus logikában. A fix osztályok és a szereposztályok formalizálhatók úgy, mint sortok (alaphalmaz), az osztályozás, mint sortokon értelmezett parciális rendezés, a dinamikus osztályok formalizálhatók úgy, mint sort

(rendező) predikátumok. Az invariánsok formalizálhatók úgy, mint nem-modális formulák, az átmenetek formalizálhatók úgy, mint akciók, melyek jelentését elő- és utófeltételes formulákkal és őrformulákkal adhatjuk meg. 8 Ez formalizálja az objektum és az osztály fogalmait és megmutatja, hogyan tudjuk megadni az objektum függvényeit (azaz műveleteit). A cikk hátralévő részében az objektum viselkedésének és kommunikációjának formalizációjához való saját megközelítését tárgyaljuk. Az elsőrendű szinten a rendszer véges számú objektumot tartalmaz, amelyek konkurens véges állapotú gépekként működnek. A tökéletes technikai közelítés következtében az objektumok azonnal kommunikálnak és végtelen végrehajtási sebességük van. Az átmenetrendszer szemantikájának alapötlete a következő: mikor egy külső esemény érkezik a rendszerhez, az hatással lehet egy vagy több objektumra, melyek mindegyike

állapotátmenet végrehajtásával reagálhat. Minden ilyen átmenet kiválthat más átmeneteket stb, amíg az összes válasz elő nem állt. Különböző módok vannak ennek pontosítására Ez az állapotgrafikon szemantika klasszikus problémája, melyhez rövidesen visszatérünk. Definiáljunk egy rendszer tranzakciót, mint egy külső esemény minden válasszal együtt, amit az esemény kiváltott, mint az esemény és válaszai együttesen atomi módon. Az atomitás itt azt jelenti, hogy a tranzakció során a rendszer nem reagál más eseményekre. Ez az elsőrendű szinten azt jelenti, hogy az átmenetben a válaszok rögtön elkészülnek. (Implementációs szinten ez azt jelenti, hogy a rendszer elég gyorsan képes előállítani a válaszokat ahhoz, hogy kész legyen a következő esemény fogadására.) Ez szinkronitási hipotézisként ismert az Esterel [3] specifikációs nyelvben. Megjegyezzük, hogy egy esemény több választ is kiválthat, mint amennyi a

tranzakcióban van. Például, egy lift hívógombjának megnyomásakor van egy közvetlen válasz, hogy meggyullad a lámpa rajta és későbbi hatás, hogy a lift megérkezik az igény kiszolgálására. Minden objektum maga is végrehajthat atomi átmeneteket, melyek a saját állapot átmenetei. Definiáljunk egy lépést úgy, mint objektum átmenetek véges halmaza, minden megjelenése az élete során különböző objektum. Az UML specifikációkhoz definiált átmenetrendszer szemantika választások a következők: - Mikor egy külső esemény érkezik, kiválthat egynél több objektum átmenetet. Ha egy objektum nemdeterminisztikus, akkor egy objektumban akár két átmenetet is kiválthat. Mivel nem hajthatóak végre ugyanabban az időben, ezek konfliktusban vannak. Ez azt jelenti, hogy általában egynél több lépés kiváltódhat, ahol minden lépés konfliktusmentes átmeneteket tartalmaz. Az első szemantikus választásunk az, hogy csak maximális számú

konfliktusmentes átmeneteket tartalmazó lépést engedélyezzük elhelyezni. - Minden objektum átmenet egy feltétellel őrzött, melynek igaznak kell lennie az átmenet végrehajtásához4. Második szemantikus választásunk az, hogy minden lépésnek van egy őrfeltétele, ami a lépésben lévő objektum átmenetek őrfeltételeinek konjunkcióját tartalmazza. Ez azt jelenti, hogy egy lépés engedélyezett, ha a benne szereplő összes átmenet engedélyezett. Együtt az első és második választásunk azt jelenti, hogy egy esemény maximális számú konfliktumentes engedélyezett objektum átmeneteket tartalmazó lépést vált ki. - Mikor egy lépés végrehajtódik, a benne szereplő összes átmenete végrehajtódik. Ez azt jelenti, hogy nincsenek lusta objektumok, amelyek nem csinálnak semmit, pedig engedélyezettek és kiváltódtak. Minden átmenetet egy objektum hajt végre és ennek az Ezt a feltételt gyakran előfeltételnek is nevezik, de jobb az őrfeltétel

kifejezés, mivel az előfeltételhez mindig tartozik egy utófeltétel. Az őrfeltétel egy speciális előfeltétel, ahol az utófeltétel igaz 4 9 objektumnak az állapotát megváltoztathatja. Feltesszük, hogy ezek a változások adottak 10 pontosan néhány formális nyelvben az elő- és utófeltételes állítások jelentése segítségével az objektum által végrehajtott akciókra. Ezek csak azt adják meg, mi változik, és nem zárják ki, hogy más dolgok ugyanúgy változhatnak. Ha egy objektum által végrehajtott minden akcióra kimondtuk, hogy „és semmi más nem változik”, akkor két különböző objektum akciói párhuzamosan nem hajthatók végre, így egy lépés nem tartalmazhat egynél több akciót. Így a „semmi más nem változik” kifejezést a lépésekre, mint egészre kell alkalmazni és nem a lépésekben lévő objektum átmenetekre. Ez lesz a harmadik szemantika választásunk. - Egy lépés generálhat eseményeket, melyek

kiválthatnak más objektumokat. Két lehetőség van ezt a szemantikát megadni. Állapotgrafikonok (statecharts) Statemate szemantikájában [16,15] ezek az események a rendszer által végrehajtott következő lépésben vannak megválaszolva. Ezt az állapotgrafikonok szekvenciális szemantikájának nevezzük Könnyen megmutatható, hogy vannak olyan rendszerek, ahol egy lépés által kiváltott válasz sohasem terminál, ha a válasz végrehajtása szekvenciális [21]. Matematikailag kellemesebb Pnueli és Shalew [26] fixpont szemantikája, melyben a kiváltott átmenetek hozzáadódnak a lépéshez. Ezt addig folytatjuk, amíg nem váltódnak ki új átmenetek a lépés által. Mivel véges számú objektum van, ez a folyamat mindig terminál A fixpont szemantika matematikailag kellemes, de intuitivitás ellen ható állapotgrafikon (statechart) viselkedéshez vezet. Emiatt egy szekvenciális lépésű szemantikát választunk Ezek a szemantikus választások megegyeznek az

UML meghatározott használatával az elsőrendű dekompozíciók bemutatására. Ezek különböznek attól, amit az UML OMG szemantikája válásakor láthatunk, mint ami informálisan körvonalazott a leíró dokumentumban [28]. Az UML állapotgrafikon (statechart) részének OMG szemantikájának formalizálására vonatkozó javaslat David Harel fejlesztésében van [13,14]. Ez a szemantika bemutatja egy UML modellt implementáló objektum-orientált program végrehajtási viselkedését. Ez alkalmazza a ROOM „az elejétől a végéig” szemantikáját [30], mint kiindulási pontot és átviszi ezt az UML-be. Az akciók ebben a szemantikában időbe telnek, és az akciók végrehajtása szekvenciális az objektum átmenetek mentén. Mikor ezen szekvencia részeként egy másik objektum művelete meghívódik, ez kiválthat egy átmenetet abban az objektumban és ez a végrehajtási folyam ismétlődik rekurzívan addig, amíg nem terminál és nem tér vissza a hívó objektum

átmenetéhez. A más objektumoknak küldött jelek egy rendszersorba kerülnek, ahol megtalálhatók kicsit később. Ezek mindegyike alkalmas az imlplementáció szintű szemantikára. Ezt a módot használva az UML grafikus programozási nyelvvé való fejlődése látszik. A fent vázolt szemantikus választások az állapotgrafikonok (statecharts) Statemate szemantikájának közelében maradnak és kiterjesztik azt szabályokkal, melyek értelmezik a pontos akció specifikációkat. Kidolgoztunk egy átmenet rendszer szemantikát a következőképpen [37]. A lépés átmenetrendszer egy gráf, melynek csúcsai jelölik a rendszer állapotait és átmenetei jelölik a lépéseket. Minden átmenet objektum akció nevek véges halmazával cimkézettek (műveletek vagy jelek nevei, melyeket az osztály diagramban deklaráltunk). Minden csúcs létező objektumok azonosító halmazával cimkézettek és minden létező objektum attribútum neveinek implementációjával. 11 Jan

Broersennel együtt megmutattuk, hogy az UML osztálydiagram és ennek állapotgrafikon (statecharts) gyűjteménye lefordítható dinamikus logikai specifikációra, mely aztán egy egyedi átmenetrendszert ad, mint szemantikát. Ebben az átmenet rendszerben minden lépés objektum átmenetek (minden olyan, ami engedélyezett) maximális halmazából áll, és minimális mértékben változtatja meg az attribútumok értelmezését. A szekvenciális végrehajtási szemantikával összhangban a jelzések, melyek más objektum átmeneteit váltják ki, a következő állapotban tárolódnak, mint igazakból álló halmaz predikátumok. Ezen szemantika formális részletei máshol találhatók. Hisszük, hogy az átmenetrendszer szemantika jó kiindulópont egy Case eszközben megvalósított végrehajtási algoritmushoz. Ezen a szemantikán alapuló algoritmust fogunk megvalósítani a jövőben TCM-ben (Toolkit for Conceptual Modeling) [8] (Eszköztár Fogalmi Modellezéshez).

Ugyanakkor, mivel az átmenet rendszerek a modális logikában előforduló értelmezési struktúrák, a szemantika használható logikai elemzéshez is. Kutatási téma lehet, annak felfedezése, hogyan lehet egy dinamikus logikai specifikációból átmenetrendszert generálni és felhasználni azt meghatározott rendszer jellemzőinek ellenőrzésére a modell ellenőrzés jelentése segítségével. Ugyanakkor, mivel a specifikáció alapvető struktúrája egy elő- és utófeltételes lista, ezt a szemantikát fel lehet használni az UML egyesítésére más formális nyelvekkel, melyek megengedik az elő- és utófeltételes stílusú specifikációt, mint a Z vagy a VDM. Hivatkozások [1] S.Austin and GI Parkin Formal methods: a survey Technical report, Division of Information Technology and Computing, National Physics Laboratory, Teddington, Middlesex United Kingdom, 31 March 1993. [2] M. Awad, J Kuusela and J Ziegler Object-Oriented Technology for Real-Time Systems: A

Practical Approch Using OMT and Fusion. Prentice-Hall, 1996 [3] G. Berry and I Cosserat The ESTEREL synchronous programming language and its mathematical semantics In S. Brookes and G Winskel, editors, Seminar on Concurrency, pages 389-448 1985 Lecture Notes in Computer Science 197. [4] P. du Bois The ALBERT II Language PhD thesis, Facultés Universitaires Notre-Dame de la Paix, Namur, 1995. [5] R.H Bourdeau and B H C Cheng A formal semantics for object model diagrams IEEE Transactions on Software Engineering, 21(70):799-821, October 1995. [6] S. Cook and J Daniels Designing Object Systems: Object-Oriented Modelling with Syntropy Prentice-Hall, 1994. [7] D. Craigen, S Gerhart and T Ralston An international survery of formal methods, volume 1: Purpose, approach, analysis and conclusion. Technical Report NISTGCR 93/626, US Department of Commerce, Technology Administration, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD 20899, 1993. [8] F.

Dehne and RJ Wieringa Toolkit for Conceptual Modeling (TCM): User’s Guide Technical Report IR401, Faculty of Mathematics and Computer Science Vrije Universiteit, De Boelelaan 1081a, 1081 HV Amsterdam, 1996. http://wwwcsvunl/~tcm [9] R.B France, J-M Bruel and MM Larrondo-Petrie An integrated object-oriented and formal modeling environment. Journal of Object-Oriented Programming, 10(7):25-34, November/December 1997 [10] H. Gomaa Software Design Methods for Concurrent and Real-Time Systems Addison-Wesley, 1993 [11] A.D Hall A Methodology for Systems Engineering Van Nostrand, 1962 12 [12] A.D Hall Three-dimensional morphology of systems engineering IEEE Transactions on System Science and Cybernetics, SSC-5(2):156-160, 1969. [13] D. Harel and E Gery Executable object modeling with statecharts In proceedings of the 18th International Conference on Software Engineering, pages 246-257. IEEE Press, 1996 [14] D. Harel and E Gery Executable object modeling with statecharts Computer,

30(7):31-42, July 1997 [15] D. Harel and A Naamad The STATEMATE semantics of statecharts ACM Transactions on Software Engineering and Methodology, 5(4):293-333, October 1996. [16] i-Logix. The Semantics of Statecharts Technical Report, i-Logix Inc, 22 Third Avenue, Burlington, Mass, 01803, U.SA, January 1991 [17] M. Jackson System Development Prentice-Hall, 1983 [18] T. Kuhn The Structure of Scientific Revolutions University of Chicago Press, second, enlarged edition, 1970. [19] I. Lakatos Proofs and Refutations Cambridge University Press, 1976 Edited by J Worall and E Zahar [20] K. Lano Enhancing object-oriented methods with formal notations Theory and Practice of Object Systems, 2(4):247-268, 1996. [21] N. Leveson, MPE Heimdahl, H Hildreth and JD Reese Requirements specification for process-control systems. IEEE Transaction on Software Engineering, 20(9):684-707, September 1994 [22] S.M McMenamin and JF Palmer Essential Systems Analysis Yourdon Press/Prentice-Hall, 1984 [23] E.

Mumford and M Weir Computer Systems in Work Design - The ETHICS Method Associated Business Press, 1979. [24] D.L Parnas and PC Clements A rational design process: How and why to fake it IEEE Transactions on Software Engineering, SE-12:251-257, 1986. [25] D.L Parnas and J Madey Functional documents for computer systems Science of Computer programming, 25:41-61, 1995. [26] A. Pnueli and M Shalev What is in a step: on the semantics of statecharts In T Ito and AR Meyer, editors, Theoretical Aspects of Computer Software, pages 244-264, Springer, 1991, Lecture Notes in Computer Science 526. [27] S. Pugh Integrated Product Engineering Addison-Wesley, 1991 [28] Rational. Unified Modeling Language: Semantics, Version 11 Rational Software Corporation, 4 September 1997. URL http://wwwrationalcom/uml/11/ 13