Verificare formală - Proiect 2

Indicaţii de modelare Încercaţi să modelaţi fiecare piesă şi subansamblu ca un proces. Piesa va avea căte o stare pentru fiecare element de procesare, iar acestea au stări care reies direct din descrierea sistemului. Trecerea unei piese de la un subansamblu la altul se modelează ca transiţie de sincronizare între piesă şi subansamblu.

Constante temporale pentru modelare:

• deplasarea pe banda de alimentare: 4.5 s
• deplasarea pe masa rotativă: 1 s
• presarea: între 10 şi 11 s (inclusiv închiderea şi deschiderea presei, paşii 1 -> 2 -> 3, pag. 14)
• deplasarea presei din poziţia de descărcare în cea de încărcare: 1 s (pasul 3 -> 1, pag. 14)
• deplasarea pe banda de depozitare: 4.5 s
• rotaţia a robotului: 1 s (pentru cate o rotatie de 45 de grade de la paşii 2 - 4, pag. 13)
• apucarea şi respectiv depozitarea piesei de către robot (incluzând mişcările de extindere/retragere a braţului): 1 s
• deplasarea macaralei: 3 s (în fiecare din sensuri, incluzând apucarea şi eliberarea piesei)

Specificaţii

• Verificaţi că sistemul e sigur, adică piesele nu sunt eliberate fără să poată fi preluate de subansamblul următor (de exemplu, nu cad de pe benzile rulante). Fixaţi pentru aceasta un număr de piese (de ex. 3), şi intervalele la care ele se află în sistem la momentul iniţial.
  Ca o alternativă, puteţi modela sistemul încorporând o logică de control care opreşte instantaneu banda rulantă când un senzor detectează că o piesă a ajuns la capăt şi ea nu poate fi preluată. Piesa e preluată apoi instantaneu când banda e repornită odată ce preluarea a devenit posibilă.
• Verificaţi că sistemul nu se blochează, şi că orice piesă e prelucrată până la sfârşit.
• Verificaţi care e timpul maxim de prelucrare pentru o piesă.
• Stabiliţi care e numărul maxim de piese care pot fi prelucrate în circuit, respectând proprietatea de siguranţă.