Formális módszerek alkalmazása együttműködő folyamatok ellenőrzésére

Napjaink komplex rendszerei komoly tervezést igényelnek. Azonban nem elég megtervezni egy rendszert, a rendszertervek ellenőrzése is szükséges, hogy megbizonyosodhassunk a helyes működésről. Különösen fontos ez az olyan kritikus rendszerek esetén, mint az elosztott felhő alapú szolgáltatások vagy a biztonságkritikus beágyazott rendszerek. Ebben segítenek nekünk a formális módszerek, amelyek a matematika eszköztárát használják fel a tervek helyességének precíz vizsgálata során.

Különösen nehéz feladat elosztott, párhuzamos és együttműködő folyamatok/rendszerek tervezése: egyre több cég vet be formális módszereket a fejlesztési folyamatban (lásd például: http://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf).

A labor során olyan egyszerű formalizmusokkal és technikákkal fogunk megismerkedni, amelyek alkalmasak arra, hogy formális módon definiáljuk a rendszerünket és azon egyszerű ellenőrzéseket végezzünk.

A labor során együttműködő folyamatokat fogunk ellenőrizni modellellenőrző eszközök segítségével.

A laborra felkészülésként a csatolt UPPAAL segédlet elolvasását, továbbá az UPPAAL eszköz letöltését és kirpóbálását javasoljuk.

A laborra érdemes saját gépet hozni, de rendelkezésre fog állni virtuális gépen az UPPAAL eszköz.

Érdeklődők számára lehetőség van kipróbálni az elmúlt években az egyetemen fejlesztett PetriDotNet modellező és analízis keretrendszert is: https://inf.mit.bme.hu/research/tools/petridotnet

Csatolt fájlok: 

UPPAAL segédlet

labor feladatok