MIT nyitóoldal
Térkép

Bemutatkozás

A csoportról
   elérhetőség
   munkatársak
   kutatás
   oktatás
   publikációk

A csoport honlapja

A Hibatűrő Rendszerek kutatócsoport oktatási tevékenysége

Informatikai technológiák szakirány

A megcélzott szakterület főbb jellegzetességei, trendjei

Az elmúlt néhány évben az informatikai technológiák robbanásszerű fejlődésének lehettünk tanúi. Az informatikai technológia, többek között, magába foglalja az adatvezérelt alkalmazások tervezési és fejlesztési aspektusait, a modell alapú, objektumorientált tervezési és megvalósítási elveket, valamint a nagy kiterjedésű IT infrastruktúrák rendszer- és szolgáltatás-felügyeleti módszereinek kérdéseit. A szakirány a korszerű technológiák által kínált új lehetőségek alapján célozza meg, hogy szakmai ismereteket rendszerezett formában, folyamatosan aktualizált tartalommal adjon át, jártasságot és alkalmazási készséget fejlesszen ki a hallgatóságban az informatikai rendszerek tervezése, fejlesztése és felügyelete során alkalmazott módszerek, eszközök és technológiák területén.

A szakirány elvégzése után a hallgatók képessé válnak:
  • adatbázisra épülő komplex (többrétegű) rendszerek megvalósítására,
  • adatbázisok teljesítményoptimalizálására,
  • kliensoldali alkalmazások fejlesztésére,
  • vékony, vastag és mobilkliensek fejlesztésére,
  • objektumorientált tervezésre és programozásra,
  • architekturális mintákat megvalósító komponensek alkalmazására,
  • szoftverek metrikák alapján történő elemzésére,
  • informatikai rendszerek teljesítményének és szolgáltatásminőségének mérésére és szabályozására,
  • IT rendszerek szűk keresztmetszeteinek meghatározására, elemzésére és javítására
  • bonyolult, sok felhasználós (pl. üzleti) IT infrastruktúrák méretezésére, ilyenek rendszerek tervezésre illetve a szervezetek IT támogató munkájába rendszermérnöki jelleggel való bekapcsolódásra.
A megszerezhető ismeretek főbb témakörei
  • Többrétegű alkalmazásfejlesztés ismerete az adattól a megjelenítési rétegig,
  • XML-alapú adatkezelés,
  • objektumorientált tervezés és programozás szabványos modelljei, programnyelvei, fejlesztő környezetei,
  • elemzési és tervezési minták, reengineering, reverse engineering, refaktorálás, antipatternek,
  • nagyvállalati rendszerfelügyelet, konfigurációmenedzsment, szoftverkarbantartás,
  • teljesítménymonitorozás, egyedi alkalmazások teljesítménymérése, felhasználó monitorozása,
  • számítógéprendszerek behatolásvédelme,
  • heterogén szoftver környezetek menedzsmentje.
A témakörökhöz kapcsolódó legfontosabb módszertanok és technológiák
  • adatvezérelt alkalmazások tervezési elvei, adatbázis-elérési technológiák,
  • MS SQL Server, Oracle Server, MySQL, ADO, OLEDB, ODBC, JDBC,
  • .NET és Java technológiák,
  • objektumorientált módszertanok, UML
  • XML, XSLT, XPath, DTD és XSD,
  • CORBA,
  • elemzési minták, reengineering, reverse engineering, refaktorálás, antipatternek
  • ITIL, ISO/IEC 17799., intelligens rendszerfelügyeleti eszközök
  • Rendszermenedzsment eszközök szabványai
Az ágazati képzés
A szakirány ágazatai a következők:
  • Rendszertervezés ágazat (MIT)
  • Rendszerfejlesztés ágazat (IIT)
  • Szoftverfejlesztés ágazat (AAIT)
Az ágazati képzés az egyes ágazatokért felelős tanszékeken elvégzendő önálló labor és szakdolgozat-készítés keretében valósul meg.

Rendszertervezés ágazat

A Rendszertervezés ágazat jellegzetességei a következőkben foglalhatók össze:

  • Komponens alapú rendszer- és alkalmazás tervezés: Az elmélyíthető tudás nem elsősorban az (alacsony szintű) programozásra, hanem az ismert elemekből, hardver és szoftver komponensekből, szolgáltatásokból való építkezésre, a rendszer architektúrájának kialakítása koncentrál. Az architektúra döntően befolyásolja az olyan rendszerszintű jellemzőket, mint a teljesítmény, megbízhatóság, biztonság.

  • Modell alapú tervezés: A rendszertervezés során hangsúlyt kapnak a korszerű modell alapú módszerek és eszközök (pl. UML, SysML leíró nyelvek használata, az architektúra változatok modell alapú elemzése és összevetése).

  • Rendszerintegrációs technológiák: Megismerhetők azok az iparban elterjedt technológiák, amelyek segítségével megvalósítható a komponensek és szolgáltatások integrálása (pl. a szolgáltatás-orientált architektúra, nagy rendelkezésre állást biztosító köztesrétegek használata).

  • Igazoltan helyes rendszertervezés: Hangsúlyt kapnak a tervezés és megvalósítás közbeni ellenőrzés módszerei (pl. a modell alapú ellenőrzés, rendszertesztelés). Ezek fokozottan előtérbe kerülnek a kritikus beágyazott rendszerekben.

  • Üzemeltetés és rendszerfelügyelet: A működés közbeni felügyeletet az ad-hoc beavatkozások helyett a szolgáltatásbiztonság alapelveit figyelembe vevő, jól tervezett folyamatok váltják fel. Ezek kialakítása mellett megismerhetők a monitorozási és konfigurációs feladatokat megvalósító eszközök.

A fenti kiemelt módszerek és technológiák az egyes témakörökben megjelent (de facto) szabványokra és ajánlásokra épülnek, így az iparban már bizonyított megoldások ismerhetők meg.

A szakirányos képzésben megszerezhető kompetenciák közül a Rendszertervezés ágazathoz kötődőek és hangsúlyosak a következők:

  • informatikai rendszerek tervezése és megvalósítása,
  • a rendszerszintű szolgáltatásminőség mérése és szabályozása, a szűk keresztmetszetek meghatározása, elemzése és javítása,
  • bonyolult, sok felhasználós (pl. üzleti) infrastruktúrák tervezése, felügyelete, a szervezetek IT támogató munkájába rendszermérnöki jelleggel való bekapcsolódás.

Példák a megismerhető eszközökre és technológiákra

  • Modell alapú rendszertervezés: Domén-specifikus nyelvek (UML profilok, SysML, AADL), tervezői rendszerek (Eclipse, VIATRA, Rational Software Architect)

  • Rendszerintegrációs technológiák: Web szolgáltatások (IBM WebSphere), workflow keretrendszerek (Domino Workflow, Websphere Business Integration Modeler), integrációs köztesrétegek (Service Availability Forum AIS), fürtözési technológiák (Linux és Windows), virtualizáció (Xen, VMWare)

  • Integrált rendszerfelügyelet: IBM Tivoli termékcsalád (Monitoring, Directory Manager), CA Unicenter, Intel vPro

  • Rendszerverifikációs és -tesztelési eszközök: Modell alapú helyességbizonyítás (Esterel SCADE), funkcionális és teljesítménytesztelés (Rational Functional Tester, Performance Tester)

Alapképzés tárgyai

Formális Módszerek

Oktatók:
dr. Pataricza András egyetemi tanár
dr. Bartha Tamás egyetemi adjunktus
A tantárgy célkitűzése
Az informatikai rendszerek méretének növekedésével mindinkább követelmény az, hogy a rendszer nem csak funkcionalitásában legyen helyes, hanem az alkalmazott implementáció bizonyítottan helyes konstrukciót eredményezzen. Ennek egyik jellegzetes trendje a formális modellekből kiinduló automatikus kódszintézis. A rendszertervezés során a kritikus elemek vizsgálatához mindinkább formális modelleken alapuló analízist alkalmaznak a rendszertervezés fázisától kezdve. A tárgy áttekintést ad az informatikai rendszerek formális minőségi és mennyiségi modelljeinek megalkotásához és analíziséhez szükséges számításelméleti háttérről, ideértve a legfontosabb matematikai leíró paradigmákat, nyelvi realizációjukat, és a kapcsolódó analitikus és szimulációs vizsgálati módszereket. Keresztmetszeti képet ad a fenti alapismeretek alkalmazásáról az informatika területén, ideértve a rendszerszintű modellezést, a hardver tervezést, a hálózati protokollok analízisét, valamint a szoftver helyességbizonyítást.

A tantárgy részletes tematikája:
  • Informatikai rendszerek minőségi analízise o A formális módszerek az informatikai rendszerek tervezésében, specifikáció, verifikáció, modellellenőrzés, helyességbizonyítás.
  • Petri ­hálók o Struktúra, dinamikus viselkedés, állapotegyenlet, token játékok, tulajdonság modellek (elérhetőség, korlátosság, élő tulajdonság, perzisztencia).
  • Petri ­hálók analízis módszerei o Elérhetőségi gráf, Martinez-Silva algoritmus, invariánsok. Redukciós technikák. Lineáris algebra alkalmazása az analízisben. Predikátumok, diagnosztikai problémák modellezése. Színezett, jól ­formált Petri ­hálók (DesignCPN).
  • Diszkrét idejű szimuláció alapjai o Petri-háló szimulátorok felépítése, szolgáltatásai. Számítógépes kísérlettervezés alapjai.
  • Alkalmazások o Real-time, konkurrens és elosztott alkalmazások modellezése. Gyártásautomatizálás és ütemezés. Digitális hardware tervezés. Workflow menedzsment. Ágens technológia formális modelljei (P-gráfok).
  • Temporális logikák o Osztályozás. Lineáris temporális logika (LTL­ kielégíthetőség és érvényesség). Elágazó idejű temporális logika (BTL). CTL és CTL
  • (érvényesség és kielégíthetőség, FairCTL). Alkalmazás konkurrens és biztonságkritikus rendszerekben. Formalizálás, komplexitás, BDD alapú reprezentáció, SMV.
  • Processz algebrák o Konkurrens nyelvek alapjai (CSP, CCS). Speciális leíróeszközök (Ada-hálók, P-gráfok).
  • Adatfolyamhálók o Modellezés adatfolyam hálókkal, modellfinomítás, konzisztencia ellenőrzés
  • Állapottérképek o Az UML dinamikaleíró eszközei (állapottérkép, aktivitás diagram, üzenetdiagram). o UML és a STATEMATE szemantika. Tervezés állapottérkép alapján.
  • Alkalmazások verifikációja és validációja o Transzformáció bázisú modellverifikáció.

Ph.D. képzés tárgyai

Szoftver verifikáció és validáció

Oktató:
dr. Majzik István egyetemi docens
A tantárgy célkitűzése A tárgy célja a professzionális szoftvertervezésben használatos formális specifikációs nyelvek, verifikációs módszerek és validációs technikák rendszerező ismertetése. Ennek keretében hangsúlyosan tárgyalja a tipikus formalizmusok és módszerek matematikai alapjait (formális nyelvek és szemantikák) valamint a korszerű tesztelési módszereket. Segítségükkel lehetővé válik algoritmusok és adatstruktúrák precíz leírása, tulajdonságaik bizonyítása és elemzése.

A tantárgy részletes tematikája:
  • 1. Bevezető: A szoftver minőség és ennek mértékei, a program és a dokumentáció minősége. A verifikáció és validáció szerepe a tervezési folyamatban. Tervezési módszertanok, fejlesztési szabványok. A szoftver és hardver verifikáció és validáció közöttti különbségek. Formális módszerek alkalmazása: Gyenge és erős formális módszerek.
  • 2. Formális specifikáció: Formális specifikációs nyelvek szerepe, ezek csoportosítása: Modell-orientált nyelvek, processz-leíró nyelvek, logikai nyelvek, Hibrid megközelítések. Objektum-orientált specifikációs nyelvek. Megbízhatósági és teljesítményjellemzők formális specifikációja (CSL sztochasztikus logika).
  • 3. Verifikáció: A formális szemantika szerepe. A formális verifikáció alapmódszerei: modell ellenőrzés, ekvivalencia ellenőrzés és tételbizonyítás. Az állapottér kezelésének módszerei (szimmetriák kihasználása, BDD). A tételbizonyítás és a temporális logikai modell ellenőrzés összekapcsolása. Megbízhatósági és teljesítményjellemzők ellenőrzése: szoftver megbízhatósági modellek, kapcsolódás a modell ellenőrzés technikáihoz.
  • 4.Program helyességbizonyítás: Matematikai alapmódszerek (strukturális és számítási indukció). Helyességi kritériumok megfogalmazása. Egyszerű determinisztikus programok bizonyítása (részleges helyesség és terminálás). Kompozicionális bizonyítás. A helyességbizonyítás gyakorlati eszközei (automatikus tételbizonyító rendszerek, kódverifikációs eszközök).
  • 5.. Validáció: Szoftver tesztelési módszerek. Hibamodellek és érvényességi körük. Funkcionális és strukturális tesztelés. A vezérlési szerkezet tesztelése. Tesztminőségi mérőszámok. Tesztelési stratégiák és folyamatok. Modulok tesztelése, izolációs tesztelés. Integrációs tesztelés és rendszertesztelés. Időzítési szempontok és tesztelésük. Objektum-orientált rendszerek tesztelése. Wrapper osztályok használata. Öröklésfüggő, állapotfüggő, szálfüggő lefedettség. Statisztikai tesztelés OO rendszerekben. Automatikus teszttervezés formális specifikáció alapján.

A modellvezérelt fejlesztés alapja

Oktató:
dr. Varró Dániel egyetemi adjunktus
A tantárgy célkitűzése Napjainkban az informatikai rendszerek modellvezérelt fejlesztése nemcsak a szoftverfejlesztés, de az általános értelemben vett rendszerfejlesztés vezető trendjévé vált. A modellvezérelt fejlesztési folyamat központi problémáját e nyelveken belüli és e nyelvek közötti modelltranszformációk matematikailag precíz leírása jelenti. A tantárgy célja, hogy mérnöki szemléletű esettanulmányok felhasználásával bemutassa a modellvezérelt tervezés matematikai alapjait és modern technológiáit. A tantárgy előadásai során olyan eszközöket és technikákat mutatunk be, melyet a hallgatók felhasználhatnak kutatásaik során felmerülő modellezési és transzformációs problémák megoldására is.

A tantárgy részletes tematikája:
  • Bevezetés: Modellvezérelt rendszertervezés Model Driven Architecture (MDA), Modellezési nyelvek helye, szerepe a modellvezérelt tervezési folyamatban, Modelltranszformációk, Rendszermodellek modelltranszformáció alapú analízise
  • Modellezési nyelvek tervezése: Modellezési nyelvek szabványai (MOF, XMI), Modellezési nyelvek formális leírása (Leíró logikák, VPM), Kényszerleíró formalizmusok (OCL, leíró logikák, gráfminták) Esettanulmány: modellezési nyelveket támogató általános keretrendszerek (IBM: EMF, Sun: MDR), Aspektus-orientált modellezés Az aspektus-orientált modellezés célja, problémái, Modellszövés, Modellbázisú kódgenerálás, Domain-specifikus modellezési nyelvek, UML Profile-ok és aspektusok kapcsolata, Esettanulmány: Schedulability, Dependability, Security aspektusok modellezése.
  • Modelltranszformációk és kódgenerátorok specifikációja: A modelltranszformáció matematikai háttere (gráftranszformáció, absztrakt állapotgépek, generikus és meta-transzformációk), Modelltranszformációs keretrendszerek (Viatra, Progres, stb.), Modellek szimulációja, Modellbázisú kódgenerálás (template-ek, modell-kód transzformációk), Automatikus nézetgenerálás, Modellkarbantartás, Modellek és transzformációk integrációja, Esettanulmányok (modelltranszformáció): PIM-PSM transzformációk, UML, BPM és BPEL transzformációk, Esettanulmányok (Kódgenerátorok): kódgenerálás UML állapottérképekben; IBM: JET, Apache: Velocity, Microsoft: CodeDOM keretrendszerek.
  • Modelltranszformációk végrehajtása: Hatékony gráfmintaillesztési algoritmusok (kényszerkielégítés, lokális keresés), Gráftranszformáció adatbázisok felett, Modelltranszformációk megvalósítása objektum-orientált nyelven, Modelltranszformációs benchmarking, Esettanulmány: transzformációk megvalósítása Java és Prolog programként.
  • Modellek és modelltranszformációk formális analízise: Modellek transzformáció bázisú verifikációja és validációja, Modelltranszformációk tesztelése, Modelltranszformációk verifikációja, Optimalizálás és modelltranszformációk. Esettanulmány: Hibamodellezés és funkcionális helyességellenőrzés BPM és UML modelleken, Adatbiztonsági ellenőrzés BPM modelleken.

Felnőttképzés tárgyai

  • Szakképzési tanfolyamok