Verification Gripper Station
The reachability graph below shows the closed loop behaviour of the gripper station of the EnAS Demonstrator. As formel model a timed Net Condition/Event System was used. The formal model of the IEC 61499 task controller was recieved automaticaly by using the TNCES-Workbench implemented at the expert system SWI-Prolog. Only the model of the plant consisting of the two valves, cylinders and sensors was created by hand, but eased up through using pre modeled timed NCES modules for actors, sensors and other plant equiment.
Afterward, this plant modeled was interconnected by condition arcs with automaticaly transformed controller model. As result we get the graph below with 1625 states. A visual verification is only possible, because of the use of the graph layouter neato, which belongs to the graph visualization packet Graphviz, and the marking of the interresting steps with spontan plant transition with different colors.
Timed NCES Model
Gripper - Station - TNCES MDL
Plant Model of the Gripper Station
Gripper - Station - TNCES Plant MDL
Actors
- lower_gripper (t1, t2) ... red
- shut_gripper (t3, t4) ... brown
Cylinders
- up and down cylinder (t5, t6 ,t7, t8)... green
- closing cylinder (t9, t10 ,t11, t12) ... blue