Verification Gripper Station
The reachability graph below shows the closed loop behaviour of the gripper station of the EnAS Demonstrator. As formel model a discrete timed Net Condition/Event System (DTNCE system) is used. The formal model of the IEC 61499 task controller iss 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 is created manualy, but eased up through using pre modeled DTNCE modules for actors, sensors and other plant equiment.
Afterwards the modeled plant is interconnected by condition arcs with the automaticaly transformed controller model. As result we get the graph below with 1533 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. Furthermore different trajectories at the state space can be visulaised with the TNCES-Workbench, as shown at the last figure.
Timed NCES Model
Plant Model of the Gripper Station
Visualisation of the trajectory to close a tin
- lower_gripper (t279, t280) ... red
- shut_gripper (t281, t282) ... brown
- up and down cylinder (t287, t288 ,t289, t290)... green
- closing cylinder (t291, t292 ,t293, t294) ... blue