Verificare formală - Proiect 3

Folosind verificatorul UPPAAL modelați (în grupuri de câte doi) un proces de fabricație și verificați câteva proprietăți temporale. Studiul de caz e descris pe larg într-o pagină dedicată. Descrierea inițială o găsiți local aici.

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:

Observație: parametrii nu sunt dați rigid; îi puteți varia și să analizați astfel efectul asupra comportamentului sistemului. Specificații În funcție de întrebări și mersul proiectului, vor apărea clarificări ulterioare.
Marius Minea
Last modified: Sat Dec 6 12:37:41 EET 2003