Bemutatók

 

Ezen az oldalon néhány esettanulmány és eszközismertető segítségével mutatjuk be a Rendszertervezés ágazathoz kötődő alkalmazási területeket és technológiákat. A bemutatókat az önálló laboratórium és szakdolgozat témakörök szerint csoportosítjuk.

Bevezetőként álljon itt egy áttekintő fóliasorozat az ágazatról, amiben bemutatjuk az ágazat tantárgyait, az önálló laboratóriumi és szakdolgozat témaköröket, a megismerhető eszközöket és technológiákat: Ágazat bemutató (PDF, 1.5 MB)
A következő fóliasorozat a Hibatűrő Rendszerek Kutatócsoport EU projektjeit tekinti át. A projektek témakörei között szerepelnek kritikus beágyazott rendszerek, web szolgáltatások, mobil ad-hoc szolgáltatásbiztos rendszerek, biztonságkritikus rendszerek: FTSRG Kutatás (PDF, 1.1 MB)

Kritikus beágyazott rendszerek

A kutatócsoport legnagyobb jelentőségú EU projektje kritikus beágyazott rendszerek területén a DECOS (Dependable Embedded Components and Systems - Szolgáltatásbiztos beágyazott komponensek és rendszerek). A projektben a modell alapú tervezési módszer és tervezői eszközök kidolgozásában vettünk részt. Az eszközök segítségével olyan demonstrátor alkalmazások készültek, mint pl. egy Airbus repülőgép csűrő szárny lemezeinek vezérlése. A mellékelt honlapon a DECOS projekt magyar nyelvű bemutató előadásai találhatók meg. A DECOS nemzeti nap előadásai
A biztonságkritikus rendszerek fejlesztési szabványai előírják számos fejlesztési illetve verifikációs és validációs módszer alkalmazását. Ezek támogatására UML állapottérkép alapú eszközöket dolgoztunk ki. A fóliasorozat röviden bemutatja a következő eszközök szerepét a fejlesztési folyamatban: (1) állapottérkép alapú szimulátor, (2) állapottérkép specifikáció statikus teljesség és ellentmondás-mentesség ellenőrző, (3) a vezérlési struktúra C forráskódjának automatikus generálása, (4) teszt esetek generálása teszt fedési kritériumok alapján, (5) futásidejű ellenőrzést és hibadetektálást megvalósító kódrészletek automatikus generálása. Biztonságkritikus rendszerek fejlesztése (FLV, 27 MB)
Beágyazott rendszerek esetén is alkalmazható a modellvezérelt fejlesztés koncepciója. A tervezett alkalmazás funkcionalitását az úgynevezett platform-független modell (PIM, Platform Independent Model) írja le, amelyet részben automatikusan lehet az adott megvalósítási platformnak (pl. CAN, FlexRay, TTP Cluster) megfelelő platform-függő modellé (PSM, Platform Specific Model) alakítani. Ez a PSM a további analízis, kódgenerálás, ellenőrzés alapja. A mellékelt bemutató a PIM-ből PSM-be való leképzés általunk kidolgozott eszköz-támogatását ismerteti. PIM-PSM leképezés (EXE, 5 MB)
Kritikus rendszerek (vasút- vagy repülésirányítás, telekommunikációs hálózatok) esetén évi maximum pár perces leállás engedhető meg. Ilyen szigorú követelményeket csak speciális módszerek alkalmazásával lehet elérni, ilyen lehet például nagy rendelkezésre állású számítógépfürtök alkalmazása. A vezető ipari cégek által megalapított Service Availability Forum szervezet (melynek a szakirányt gondozó Hibatűrő csoport volt az első akadémiai tagja) célja ilyen környezethez készített köztes rétegek (middleware-ek) szabványosítása. Egy egyszerű mintaalkalmazás segítségével bemutatjuk, hogy hogyan lehet egy ilyen SA Forum alapú rendszerrel nagy rendelkezésre állású alkalmazásokat készíteni. Nagy rendelkezésre állású alkalmazások készítése (Xvid videó, 50 MB)

Üzleti folyamatok és alkalmazások

A fóliasorozat az üzleti folyamatok formális verifikációjának területén elért eredményeinket összegzi. A Business Process Execution Language (BPEL) nyelvet napjainkban egyre gyakrabban használják végrehajtható üzleti folyamatok implementálására. Ezek a folyamatok kritikus szerepet töltenek be az intézményekben, hiszen alapvető tevékenységeket irányítanak. Ennek megfelelően a munkafolyamatok minőségének biztosítására nagy hangsúlyt kell fektetni. Mi modell ellenőrzési technikát javaslunk a munkafolyamatok egyes tulajdonságainak ellenőrzésére. A BPEL munkafolyamatokon modell absztrakciót hajtunk végre, majd a Symbolic Analysis Laboratory (SAL) modell ellenőrző használatával bizonyítunk temporális logikákkal megfogalmazott követelményeket. Üzleti folyamatok modellezése (PDF, 280 kB)
Napjainkban az egyik legfontosabb kérdés a meglévő informatikai rendszerek integrációja, az elérhető szolgáltatások kombinációjával összetett üzleti szolgáltatás építése. Ennek gyakran használt technológiája a web szolgáltatások, és az ehhez kapcsolódó szabványok, melyek célja, hogy heterogén, megbízhatatlan környezetben is tervezhető minőségű szolgáltatást biztosítsunk. A "Szolgáltatás-orientált rendszerek modell alapú tervezése- SENSORIA" EU FP6 nemzetközi kutatási projekt célja olyan módszerek és eszközök kifejlesztése, melyek segítségével a mai ipari fejlesztőkörnyezetekben elérhető funkciók mellett a rendszer helyes viselkedését, teljesítmény- és biztonsági jellemzőit tervezési időben a mérnöki modellből kiindulva ellenőrizni lehet, valamint kód generálható (szabványos telepítési leírók és kódvázak formájában). A különböző fejlesztőeszközök OSGI és Eclipse technológiák használatával integrálhatóak, így egy testreszabható fejlesztőkörnyezet hozható létre. A bemutató fóliasorozat a SYSTEMS2007 informatikai szakkiállításon is szerepelt, mely Németország második legnagyobb ilyen jellegű rendezvénye. SENSORIA projekt (FLV, 44 MB)

Rendszerfelügyelet

A videó egy diplomatervként készült kísérleti környezetet mutat be, amely az "autonóm számítástechnika" területén alkalmas algoritmusok vizsgálatára. A kísérleti környezet olyan technológiákat integrál, mint az IBM Tivoli Intelligent Orchestrator és a Matlab 7. Autonóm számítástechnika (WMV, 12 MB)

Modell alapú rendszertervezés és verifikáció

Az forráskód szintézis absztrakt szoftvermodellek automatikus forrásnyelvi szintű megvalósítását jelenti. Az alábbi előadás az UML nyelvre mint absztrakt specifikációs formalizmusra építve vázolja, hogyan oldottuk meg viselkedési modellek (UML állapottérképek) automatikus leképzését az ANSI-C programozási nyelvre. A megoldásunk célplatformjául a legnagyobb kihívást jelentő erőforrásokban szegény beágyazott rendszereket választottuk. Az előadás először sorra veszi, hogy az UML diagramjai milyen, az automatikus forráskód szintézis szempontjából érdekes információt hordoznak, ezután vázolja az állapottérképek eszközkészletét (egyszerű állapotok, állapotfinomítás, konkurens működés, pszeudoállapotok, stb.), röviden összefoglalja az állapottérképekhez kidolgozott formális szemantikát majd egy animáció sorozaton megmutatja, hogyan fut egy egyszerű példából (közlekedési lámpa) generált program egy "mitmóton" (ez a tanszék oktatási célű beágyazott platformja). A példa azt demonstrálja, hogyan tudunk vizuálisan modellezni, a modellből automatikusan forráskódot előállítani (ANSI-C-t) végül a forrást lefordítva sikeresen futtatjuk azt egy 8-bites mikrokontrollerre épülő eszközön. A videoban a slide-okat gombnyomásra lehet léptetni (zöld gomb a jobb alsó sarokban, vagy a lejátszó Play gombja bal oldalt lent), az animáció magától fut. Kódgenerálás (SWF, 20 MB)
A modellvezérelt fejlesztés során a rendszer modellje alapján lehetőség nyílik a későbbi implementáció helyességét ellenőrizni képes teszt esetek generálására. A strukturális tesztelés során olyan teszt eseteket kell generálnunk, amelyek a tesztelt alkalmazás belső állapotainak, állapotátmeneteinek minél nagyobb részét lefedik. Az itt bemutatott módszer segítségével UML állapottérkép diagramok alapján tudunk automatikusan teszteket generálni, egy külső modell ellenőrző eszközt felhasználva. A teszt generálás érdekessége, hogy - megfelelő kiindulási modell esetén - a valósidejű működést is figyelembe vevő teszt szekvenciákat generál (tehát a teszt hívások közötti időt is megadja). Tesztgenerálás (PDF, 900 kB)
Nagy megbízhatóságú rendszerek tervezése során fontos, hogy a megbízhatósági jellemzők már a tervezési folyamat során megbecsülhetőek legyenek, hiszen ennek függvénye lehet, hogy egy adott architektúra megfelel-e a rendszerrel szemben támasztott követelményeknek. Az úgynevezett megbízhatósági modellek segítségével a tervezési fázis során összevethetőek különböző architektúrák és megoldások, és így kiválasztható a tervező céljainak leginkább megfelelő változat. A megbízhatósági modell egy absztrakt matematikai modell, amely leírja az egyes komponensek meghibásodási és javítási folyamatait, valamint a komponensek közötti hibaterjedést. A modell alapján így meghatározható, hogy a komponens hibák hatására milyen gyakorisággal adódik rendszerszintű hibajelenség. A fóliasorozat azt az általunk fejlesztett eszközt mutatja be, ami UML architektúra modellek alapján konstruál megbízhatósági modelleket. Megbízhatósági elemzés (PDF, 200 kB)

 

---

Valid HTML and CSS