Aplikácia technológií virtuálnej reality ako inovačného prostriedku pri výučbe formálnych metód

Basic informations

Thematic area: komisia č. 2 pre nové technológie, metódy a formy vo vzdelávaní

Project name (Slovak): Aplikácia technológií virtuálnej reality ako inovačného prostriedku pri výučbe formálnych metód

Project name (English): Application of Virtual Reality Technologies in Teaching Formal Methods

Start of project: 2012

End of project: 2014

Condition of project: Ukončený

Project number: 050TUKE-4/2012

Project leader: Ing. Štefan Korečko, PhD.

University: Technická univerzita v Košiciach

Department: Fakulta elektrotechniky a informatiky

Anotácia originálnych výsledkov riešenia projektu v slovenskom jazyku

Výsledky tohto projektu umožňujú použiť to, čo je medzi študentmi populárne na naučenie sa niečoho čo, populárne nie je. Tou populárnou vecou sú počítačové hry, ktoré nám sprostredkujú zážitky vo virtuálnych svetoch. Nepopulárnou vecou sú takzvané formálne metódy vývoja spoľahlivého softvéru, ktoré vyžadujúce dobré matematické znalosti najmä z logiky.  Najvýznamnejším výsledkom projektu je úprava železničných simulátorov Train Director a Open Rails tak, aby reprezentovali virtuálnu železnicu pre ktorú je možné pomocou formálnych metód vytvoriť korektný riadiaci program. Virtuálna železnica je tvorená železničnou traťou po ktorej premávajú vlaky jazdiace podľa grafikonu, resp. ovládané hráčom. Trate obsahujú zariadenia ako sú výhybky a semafory. A tieto zariadenia sú ovládané riadiacim programom, vyvinutým pomocou formálnej metódy. Vďaka použitiu železničného prostredia vieme ľahko ukázať dôležitosť formálnych metód: formálne metódy nám pomáhajú vytvárať spoľahlivý softvér a riadiaci systém železnice musí byť spoľahlivý, inak môžu zahynúť ľudia. Ďalšie zaujímavé výsledky projektu sú vedecká monografia zameraná na formálne metódy B-metóda a Petriho siete a 3D editor a simulátor Petriho sietí.

Description of original results of the project in English

Results of this project allow us to use something that is popular among student to teach them something not popular. The popular things are computer games and unpopular ones are so-called formal methods for reliable software development, which require a good knowledge of mathematics, especially of formal logic. The most important result of the project are modifications of railway simulators Train Director and Open Rails in such a way that they can represent a virtual railway for which a reliable control program can be developed using formal methods. The virtual railway is about track layouts where trains run according to a schedule or commands from a player. The layouts contain devices like switches and signals, which can be operated by a control program, developed using the formal methods. Thanks to the use of the railway environment it is easy to show why formal methods are important: Formal methods help us to develop reliable software and a control system for railway has to be reliable, otherwise people can die. Other interesting outcomes of the project are a 3D editor and simulator of Petri nets and a monograph focused on formal methods B-Method and Petri nets.

Financial grant of MŠVVandŠ SR within KEGA

Financial grant of MŠVVandŠ SR within KEGA Capital expenditures in €
Drawn in year 2012 3 668,00 0,00
Drawn in year 2013 3 978,00 0,00
Drawn in year 2014 3 097,00 0,00
Pumped for the entire period of the project 10 743,00 0,00

List of project outcomes for the entire solution

Publishing activity

Category code Specific output, name (ISBN, number of pages a i.)
AFD Korečko, Štefan (50%); Dudláková, Zuzana (50%): Verified controller for simulated railway scenario. 2012 Košice : FEI TU, 2012 : ISBN 978-80-8143-049-7
AFC Hrozek, František (30%); Sobota, Branislav (25%); Korečko, Štefan (25%); Ivančák, Peter (10%); Varga, Martin (10%): Life cycle of virtual reality system – analysis step. 2012 Brno : University of Technology, 2012 : ISBN 978-80-214-4576-5
AFD Hrozek, František (34%); Sobota, Branislav (33%); Korečko, Štefan (33%): Use of virtual-reality technologies in education. 2012 Trenčín : TU Alexandra Dubčeka, 2012 : ISBN 978-80-8075-538-6
AED Korečko, Štefan (60%); Natafaluši, Peter (40%); Kocur, Dušan (0%); Levický, Dušan (0%): 3D Engines for Visualization of Formally Developed Control Systems. 2012 Košice : FEI TU, 2012 : ISBN 978-80-553-0890-6
AED Kolesár, Matúš (10%); Steingartner, William (90%); Kocur, Dušan (0%); Levický, Dušan (0%): How to Express an Action Semantics of Programming Languages in Categories. 2012 Košice : FEI TU, 2012 : ISBN 978-80-553-0890-6
AED Martinko, Tomáš (10%); Steingartner, William (90%); Kocur, Dušan (0%); Levický, Dušan (0%): How to Express Denotational Semantics in Categories. 2012 Košice : FEI TU, 2012 : ISBN 978-80-553-0890-6
AED Polák, Marián (10%); Steingartner, William (90%); Kocur, Dušan (0%); Levický, Dušan (0%): The rôle of Abstract Data Types and Abstract Behavior Types. 2012 Košice : FEI TU, 2012 : ISBN 978-80-553-0890-6
AFD Steingartner, William (100%): The rôle of categorical structures in integral calculus. 2012 Košice : FEI TU, 2012 : ISBN 978-80-8143-049-9
ADE Steingartner, William (100%): Toposes are symmetric monoidal closed categories. 2012 ISBN 1731-5417
AFD Sobota, Branislav (20%); Hrozek, František (30%); Korečko, Štefan (20%); Ivančák, Peter (10%); Varga, Martin (10%); Dudláková, Zuzana (10%): Virtual Reality and its Technologies in Education – Our Experiences. 2012 Košice : Elfa, 2012 : ISBN 978-1-4673-5123-2
ADE Sobota, Branislav (40%); Korečko, Štefan (40%); Hrozek, František (20%): On building an object-oriented parallel virtual reality system. 2012 ISSN 2081-9935
ADE Korečko, Štefan (60%); Hudák, Štefan (30%); Doboš, Jozef (5%); Šimoňák, Slavomír (5%): De/compositional Mw automaton-based reachability algorithm. 2013 ISSN 1110-2586
AED Sorád, Ján (45%); Korečko, Štefan (45%); Dudláková, Zuzana (10%); Kocur, Dušan (0%); Pietriková, Alena (0%): An External Programming Control of Track Devices in Train Simulators. 2013 Košice : FEI TUKE, 2013 : ISBN ISBN 978-80-553-1440-2
AFC Dudláková, Zuzana (50%); Varga, Martin (50%): Different approaches to utilisation of formal methods. 2013 Prague : Czech Technical University in Prague, 2013 : ISBN 978-80-01-05242-6
AFD Dudláková, Zuzana (50%); Varga, Martin (50%): Verified Software Development using B-Method. 2013 Košice : TU, 2013 : ISBN 978-80-553-1422-8
AFC Varga, Martin (50%); Dudláková, Zuzana (50%): Markerless augmented reality using head tracking device. 2013 Prague : Czech Technical University in Prague, 2013 : ISBN 978-80-01-05242-6
AFD Varga, Martin (50%); Ivančák, Peter (50%): Markerless augmented reality using electromagnetic tracking device. 2013 Košice : TU, 2013 : ISBN 978-80-553-1422-8
AAB Sobota, Branislav (50%); Hrozek, František (50%); Sinčák, Peter (0%); Šujanský, Milan (0%): Virtuálna realita a jej technológie. 2013
AFA Sobota, Branislav (60%); Hrozek, František (40%): Virtuálna realita a jej technológie. 2013 Ostrava : VŠB-TU, 2013 : ISBN 978-80-248-3189-3
AFD Sobota, Branislav (40%); Korečko, Štefan (30%); Hrozek, František (30%): Mobile Mixed reality. 2013 Danvers : IEEE, 2013 : ISBN 978-1-4799-2161-4
ADF Hrozek, František (100%): 3D interfaces of systems. 2013 ISSN 1338-1237
AED Benčková, Martina (50%); Steingartner, William (50%); Kocur, Dušan (0%); Pietriková, Alena (0%): The Case Study for Selected Problems of Recursion in Informatics. 2013 Košice : FEI TU, 2013 : ISBN 978-80-553-1440-2
AED Hunčovský, Václav (25%); Steingartner, William (75%); Kocur, Dušan (0%); Pietriková, Alena (0%): Introduction to session types. 2013 Košice : FEI TU, 2013 : ISBN 978-80-553-1440-2
AFC Steingartner, William (50%); Korečko, Štefan (25%); Porubän, Jaroslav (25%): Some categorical structures and their rôle in differential calculus. 2013 Varaždin : University of Zagreb, 2013 : ISSN 1847-2001
AFC Korečko, Štefan (80%); Sorád, Ján (10%); Dudláková, Zuzana (5%); Sobota, Branislav (5%): A Toolset for Support of Teaching Formal Software Development. 2014 Švajčiarsko : Springer, 2014 : ISBN 978-3-319-10430-0 ISSN 0302-9743
AFC Experiences with Virtual Reality Technologies in Education Process / Branislav Sobota ... [et al.]- 2014.In: ITRO 2014 : international conference on Information Technology andDevelopment of Education : proceedings : Zrenjanin, June, 2014. - Zrenjanin : University of Novi Sad, 2013 P. 11-15. - ISBN 978-86-7672-225-9
AFC Virtual User Interface / Branislav Sobota ... [et al.]- 2014.In: ITRO 2014 : international conference on Information Technology andDevelopment of Education : proceedings : Zrenjanin, June, 2014. - Zrenjanin : University of Novi Sad, 2014 P. 77-80. - ISBN 978-86-7672-225-9
ADE Augmented Reality with Interactive Interfaces / Martin Varga, Branislav Sobota, František Hrozek ... [et al.]- 2014.In: Studia Universitatis Babes-Bolyai : Series Informatica. Vol. 59, no. 2 (2014), p. 21-33. - ISSN 2065-9601
ADM Korečko, Štefan (70%); Sobota, Branislav (30%): Petri nets to B-language transformation in software development. 2014 ISSN 1785-8860
AAB Korečko, Štefan (80%); Hudák Štefan(20%): Formálne metódy pre diskrétne systémy: Petriho siete a B-metóda, Technická univerzita v Košiciach 140s., ISBN 978-80-553-1895-0
ABC Korečko, Štefan (99%); Sorád, Ján (1%): Using Simulation Games in Teaching Formal Methods for Software Development, In: Innovative Teaching Strategies and New Learning Paradigms in Computer Programming, IGI Global, 2015 (v tlači)
AAA Milan Guzan, Branislav Sobota Vizualizácia stavového priestoru nelineárnych autonómnych obvodov, 1. vyd., Ostrava, Česká republika: JUPOS - 2015. - 138 s.. - ISBN 978-80-87321-31-7.25
AFD Semi-immersive virtual reality system with support for educational and pedagogical activities / Ladislav Jacho, Branislav Sobota, Štefan Korečko, František Hrozek - 2014. In: ICETA 2014 : 12th IEEE International Conference on Emerging eLearning Technologies and Applications : proceedings : December 4-5, 2014, Stary Smokovec, Slovakia. - Danvers : IEEE, 2014 P. 199-204. - ISBN 978-1-4799-7738-3

Final evaluation of the commission KEGA

Splnil ciele výborne.

Filter

Filter