Formális módszerek - Házi feladat 29-35

Ez az oldal a korábbi SCH wiki-ről lett áthozva. Az eredeti változata itt érhető el.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor kérlek javíts rajta egy rövid szerkesztéssel.

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót

30. Vérkeringés

Konzulens: Sisak Áron, email: sa438@hszk.bme.hu

34. Hibás FTP szerver

Konzulens: Vágó Dávid, honlap, email: vd419@hszk.bme.hu

Jó tudni

Lásd a 10. feladatnál leírtakat, továbbá:

• Az elemezhetőség végett tényleg lehet brutálisan egyszerűsíteni a modellt. Nálam a végére két processz maradt az ötből, melyekkel maximum két műveletet tudott végrehajtani a felhasználó az automatikus kiléptetés előtt. A Promelás modell ellenőrzésekor volt olyan LTL, amelynél csak egy processzt vizsgáltam. Olyan ellenőrzéseket nem is csináltam, ami több mint egy percig tartott volna a gépemen.
• A merevlemez hibáját nálam egy nyelő tranzíció jelentette, ami esetenként elnyelte a winyóba "dobott" tokent. Az nem a legjobb megoldás, ha a javított verzióban elhagyod ezt a tranzíciót (hiszen ez lényegében ugyanaz, mintha kicserélnéd a winyót egy újra). Szebb, ha ebből a tranzícióból továbbvezeted a tokent valamilyen hibakezelő ágként. (Mondjuk nekem az előző verziót is elfogadták.)
• Állítólag az is megfelelő (csak hogy egyszerű legyen), ha nem pont az a processz száll el, amelyik belefutott a hibás szektorba, hanem bármelyik másik, amelyik ugyanazt a winyót használja
• Nálam a sima állpotgéppel sem volt probléma, nem UML-t rajzoltam.

-- palacsint - 2006.05.22.