Project Details
Ověřování temporálních vlastností modelů popsaných objektově orientovanými Petriho sítěmi
Project Period: 1. 1. 1998 - 31. 12. 1998
Project Type: grant
Code: FEI-98-?
Agency: Faculty of Electrical Engineering and Computer Science BUT
Program:
Object-oriented Petri nets, temporal logics, model checking, state space explosion
The goal of this project is to allow model checking of temporal formulae over models described by OOPNs. To achieve this goal, it is necessary to define the notion of the name abstracted state space of OOPNs, to propose a suitable temporal logic for specifying properties of OOPN based models, and to develop some model checking procedure for checking validity of formulae of this logic. It is also unavoidable to fight against the state explosion problem in some way. Here, it is supposed that we will be able to modify methods known from the area of coloured Petri nets and make them work also in the context of the more dynamical OOPNs.
1998
- VOJNAR Tomáš. An Overview of Some Automated Tools for Formal Analysis and Verification. In: Proceedings of 20th International Workshop on Advanced Simulation of Systems ASIS'98. Krnov, 1998, pp. 223-228. ISBN 80-85988-26-7. Detail
- JANOUŠEK Vladimír and VOJNAR Tomáš. Modelling a Flexible Manufacturing System. In: Proceedings of 32nd Spring International Conference on Modelling and Simulation of Systems MOSIS'98. Sv. Hostýn, 1998, pp. 195-200. ISBN 80-85988-23-2. Detail
- ČEŠKA Milan, JANOUŠEK Vladimír and VOJNAR Tomáš. Object-Oriented Petri Nets, Their Simulation, and Analysis. In: Proceedings of the IEEE SMC'98 Conference. San Diego, California: unknown, 1998, pp. 256-261. ISBN 0-7803-4781-1. ISSN 1062-922X. Detail
- JANOUŠEK Vladimír and VOJNAR Tomáš. State Spaces of Object-Oriented Petri Nets. In: Proceedings of MFCS'98 Workshop on Concurrency. Brno: unknown, 1998, pp. 87-96. Detail