Verificare formală - Proiect 2

Folosind verificatorul UPPAAL modelați 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.
Arhiva cu versiunea curenta de UPPAAL o gasiti 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


Marius Minea
Last modified: Tue Nov 9 12:19:20 EET 2004