| Seznam |
| Téma: | Automatic generation of finite automata from production line models |
|---|---|
| Vedoucí: | Pavel Burget |
| Vypsáno jako: | Práce v týmu a její organizace |
| Popis: | The purpose of this project is to build formal model of a production process such a robotic welding or painting line. Such production lines are widely used in automotive industry. Before physical realization they are designed by the manufacturing process planners in specialized tools such as Tecnomatix Process Designer, Process Simulate or Tecnomatix Manufacturing. Such designs contain not only the layout of the line and the kinematics of the machines but also operations and their order as they are executed by the machines.
1. Study how production lines are represented in Process Simulate. 2. Design a general timed automata representation. 3. Design an approach for representing the production lines as timed automata. 4. Implement the transformation from the Process Simulate representation into the model from point 2. 5. Implement export from the created representation to an existing model checker such as UPPAAL. 6. Study existing approaches to the translation of PLC programs into timed state machines. 7. Implement a general timed state machine representation. 8. Implement a selected approach and test it with Siemens PLC. 9. Perform the verification of the selected properties. It is possible to do a follow-up project as a master thesis. Having the formal models (finite automata) allows to use the model for verification and/or testing of the correct behavior of the controllers. One part of the team will generate the models from the production line (points 1-5 bellow), the other part will generate the models from the PLC programs (points 6-8 bellow) and both part will cooperate on point 9. |
| Pokyny: | 1. Study how production lines are represented in Process Simulate.
2. Design a general timed automata representation. 3. Design an approach for representing the production lines as timed automata. 4. Implement the transformation from the Process Simulate representation into the model from point 2. 5. Implement export from the created representation to an existing model checker such as UPPAAL. 6. Study existing approaches to the translation of PLC programs into timed state machines. 7. Implement a general timed state machine representation. 8. Implement a selected approach and test it with Siemens PLC. 9. Perform the verification of the selected properties. It is possible to do a follow-up project as a master thesis. |
| Realizace: | C#, XML, Step7, UPPAAL |
| Vypsáno dne: | 01.02.2018 |
| Max. počet studentů: | 4 |
| Přihlášení studenti: | |