Formal Verification - Project 2

Modeling hints Try to model each piece or subsystem as a process. The piece will have a state for each processing elements, and these have states which directly correspond to the system description. Progress of the piece from one processing element to the next is modeled as a synchronization transition with the processing subsystem.

Temporal constants for modeling:

• transit time on feed belt: 4.5 s
• time on rotating table: 1 s
• pressing: between 10 and 11 s (including opening and closing the press, steps 1 -> 2 -> 3, p. 14)
• moving the piece from unloading to loading position: 1 s (step 3 -> 1, p. 14)
• transit time on deposit belt: 4.5 s
• rotating the robot: 1 s (for each 45 degree rotation in steps 2 - 4, p. 13)
• grasping and depositing the piece by the robot (including extending and retracting the arm): 1 s
• moving the crane: 3 s (in each direction, including grasping and releasing the piece)

• Check that the system is safe, i.e., pieces cannot be freed without being taken by the next subsystem (e.g., don't fall off the moving belts). For this purpose, fix a number of pieces (e.g., 3), and the intervals at which they initially arrive on the feedbelt.
• Verify that the system does not deadlock, and each piece is processed completely.
• Check the maximum processing time for each piece.
• Determine the maximal number of pieces which can be processed in a loop, respecting the safety property.