Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail projektu
Období řešení: 1.1.2007 — 31.12.2009
Zdroje financování
Grantová agentura České republiky - Standardní projekty
O projektu
Vysokoúrovňový návrh a formální verifikace jsou jednou z perspektivních cest, jak dosáhnout vyšší spolehlivosti a bezpečnosti počítačových systémů. Předkládaný projekt navazuje na zkušenosti a výsledky řešitelského týmu a na existující spolupráci se špičkovými zahraničními pracovišti a koncipuje základní výzkum takových pokročilých formálních přístupů, vycházejících z teorie systémů, logiky, teoretické informatiky a umělé inteligence, které jsou aplikovatelné v oblastech vysokoúrovňového návrhu a formální verifikace. Předpokládá, že tyto přístupy mohou výrazně pomoci tam, kde metody verifikace založené na hrubé síle selhávají. Projekt zahrnuje výzkum vzájemně se doplňujících metod návrhu založeného na modelech, simulační verifikaci a model checkingu konečně i nekonečně stavových systémů. Jedná se primárně o výzkum nových přístupů, metod a jejich vlastností, možných rozšíření či specializací apod. Metody vyvíjené v projektu budou prototypově implementovány a ověřeny na vhodných případových studiích. [private wiki (http://perchta.fit.vutbr.cz/intelligentsystems/103)]
Popis anglickyHigh-level design and formal verification are promising approaches for improving reliability and safety of computer systems. This project is proposed by the highly experienced team with the expressive results and the international cooperation with the prestigious research teams. The project aims to explore and use advanced formal approaches from the fields like system theory, logics, theoretical computer science, and artificial intelligence in the area of the high-level design and formal verification. We believe that these approaches can significantly improve the verification abilities, especially in the cases on which the brute-force approach does not succeed. The proposed research project covers complementary methods, i.e., the model-driven design, the simulation-based verification, and the model checking of finite-state as well as infinite-state systems. The research should result in developing new approaches and methods with unique properties. These methods will be validated by the prototype implementation and will be evaluated by suitable case studies.
Klíčová slova formální modely, simulační verifikace, formální verifikace, model checking
Klíčová slova anglickyformal models, simulation verification, formal verification, model checking
Označení
GA102/07/0322
Originální jazyk
čeština
Řešitelé
Češka Milan, prof. RNDr., CSc. - hlavní řešitelCerhák Michal, Ing. - spoluřešitelErlebach Pavel, Ing., Ph.D. - spoluřešitelHolík Lukáš, doc. Mgr., Ph.D. - spoluřešitelJanoušek Vladimír, doc. Ing., Ph.D. - spoluřešitelKironský Elöd, Ing. - spoluřešitelKočí Radek, Ing., Ph.D. - spoluřešitelKřena Bohuslav, Ing., Ph.D. - spoluřešitelPolášek Petr, Ing., Ph.D. - spoluřešitelRogalewicz Adam, doc. Mgr., Ph.D. - spoluřešitelSmrčka Aleš, Ing., Ph.D. - spoluřešitelVojnar Tomáš, prof. Ing., Ph.D. - spoluřešitel
Útvary
Ústav inteligentních systémů- odpovědné pracoviště (1.1.1989 - nezadáno)Výzkumná skupina automatizované analýzy a verifikace - VeriFIT- interní (1.2.2007 - 31.12.2009)Výzkumná skupina modelování a optimalizace- interní (1.2.2007 - 31.12.2009)Ústav inteligentních systémů- spolupříjemce (1.2.2007 - 31.12.2009)
Výsledky
JANOUŠEK, V.; KIRONSKÝ, E.: xx; SmallDEVS-07. xx. URL: http://www.fit.vutbr.cz/~janousek/smalldevs/. (Software)Detail
KONEČNÝ, F.; VOJNAR, T.; BOZGA, M.; IOSIF, R.: xx; FLATA. xx. URL: http://www-verimag.imag.fr/FLATA.html. (Software)Detail
LETKO, Z.; VOJNAR, T.; KŘENA, B.: xx; Java Race Detector & Healer. xx. URL: https://www.fit.vut.cz/research/product/49/. (Software)Detail
LETKO, Z.; VOJNAR, T.; KŘENA, B.: xx; Java Atomicity Violation Detector & Healer. xx. URL: https://www.fit.vut.cz/research/product/90/. (Software)Detail
KOČÍ, R.: xx; PNtalk. xx. URL: https://www.fit.vut.cz/research/product/66/. (Software)Detail
ŠIMÁČEK, J.; HOLÍK, L.; VOJNAR, T.: xx; Tool for Computing Simulations. xx. URL: https://www.fit.vut.cz/research/product/131/. (Software)Detail
KŘENA, B.; BRAIONE, P.; DENARO, G.; PEZZE, M.: xx; Model checking Using Symbolic Execution. xx. URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/muse/. (Software)Detail
IOSIF, R.; VOJNAR, T.; HABERMEHL, P. A Logic of Singly Indexed Arrays. Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 558-573. ISBN: 978-3-540-89438-4.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. FIT-TR-2008-005, Brno: 2008. 18 p.Detail
SKLENÁŘ, J.; CUTARAJ, V.; ČEŠKA, M. Using Integer Programming for Discrete Problem Optimization. The 2008 European Simulation and Modelling Conference. EUROSIS-ETI Publications. LE HAVRE: EUROSIM-FRANCOSIM-ARGESIM, 2008. p. 19-21. ISBN: 978-90-77381-44-1.Detail
HABERMEHL, P.; IOSIF, R.; VOJNAR, T. What else is decidable about integer arrays?. TR-2007-8, Grenoble: VERIMAG, 2008. 36 p.Detail
JANOUŠEK, V.; KOČÍ, R. The PNtalk/SmallDEVS Framework -- Meta-level Modeling Techniques. Proceedings of CSE 2008 International Scientific Conference on Computer Science and Engineering. Košice: elfa, s.r.o., TU Kosice, 2008. p. 16-23. ISBN: 978-80-8086-092-9.Detail
HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. FIT-TR-2009-03, Brno: 2009. 17 p.Detail
MAZAL, Z.; KOČÍ, R.; JANOUŠEK, V.; ZBOŘIL, F. Modelling intelligent agents for autonomic computing in the PNagent framework. International Journal of Autonomic Computing, 2009, vol. 1, no. 2, p. 121-139. ISSN: 1741-8569.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 212-222. ISBN: 978-3-540-70843-8.Detail
HOLÍK, L. Simulations and Antichains for Efficient Handling of Finite Automata. Brno: Department of Intelligent Systems FIT BUT, 2011. 128 p.Detail
JANOUŠEK, V.; KIRONSKÝ, E.; POLÁŠEK, P. An Architecture for Simulation-Based Evolutionary Design of Systems. Proceedings of the 16th International Conference on System Science. Systems Science 2007, volume 1. Wroclaw: Wroclaw University of Technology, 2007. p. 396-405. ISBN: 978-83-7493-339-1.Detail
BOZGA, M.; IOSIF, R.; KONEČNÝ, F. Fast Acceleration of Ultimately Periodic Relations. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2010. p. 227-242. ISBN: 978-3-642-14294-9.Detail
LETKO, Z. An Architecture for Self-Healing of Data Races and Atomicity Violations for Java. Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Brno University of Technology, 2008. p. 256-258. ISBN: 978-80-214-3615-2.Detail
POLÁŠEK, P.; JANOUŠEK, V. Modeling and Simulation Management in Distributed Environment Using Web Services. Proceedings of the 14th International Congress of Cybernetics and Systems of WOCS. Wroclaw: Wroclaw University of Technology, 2008. p. 1-9. ISBN: 978-83-7493-400-8.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Computing Simulations over Tree Automata: Efficient Techniques for Reducing Tree Automata. FIT-TR-2008-001, Brno: 2008. 34 p.Detail
KOČÍ, R.; MAZAL, Z.; ZBOŘIL, F.; JANOUŠEK, V. Modeling Deliberative Agents Using Object Oriented Petri Nets. Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007. p. 15-20. ISBN: 0-7695-2976-3.Detail
ABDULLA, P.; HOLÍK, L.; CHEN, Y.; VOJNAR, T. Mediating for Reduction (On Minimizing Alternating Büchi Automata). Brno: Faculty of Information Technology BUT, 2009. 26 p.Detail
JANOUŠEK, V.; KOČÍ, R.; MAZAL, Z.; ZBOŘIL, F. PNagent: a Framework for Modelling BDI Agents using Object Oriented Petri Nets. Proceedings of 8th ISDA. Los Alamitos: IEEE Computer Society, 2008. p. 420-425. ISBN: 978-0-7695-3382-7.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. FIT-TR-2008-004, Brno: 2008. 19 p.Detail
MAZAL, Z.; JANOUŠEK, V.; KOČÍ, R. Enhancing the PNtalk Language with Negative Predicates. MOSIS '08. Ostrava: Marq software s.r.o., 2008. p. 28-34. ISBN: 978-80-86840-40-6.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Computing Simulations over Tree Automata (Efficient Techniques for Reducing Tree Automata). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 93-108. ISBN: 978-3-540-78799-0.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Faculty of Informatics MU, 2008. p. 3-11. ISBN: 978-80-7355-082-0.Detail
JANOUŠEK, V.; KIRONSKÝ, E. Reflective Framework for Interactive Modeling and Simulation of Intelligent Systems. Proceedings of Nineteenth International Conference on Systems Engineering 19-21 August 2008 Las Vegas, Nevada. Los Alamitos: IEEE Computer Society, 2008. p. 480-485. ISBN: 978-0-7695-3331-5.Detail
IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. Computer Aided Verification. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 157-172. ISBN: 978-3-642-02657-7.Detail
JANOUŠEK, V.; KIRONSKÝ, E. Interactive evolutionary modelling and simulation of discrete-event systems using prototypical objects. International Journal of Autonomic Computing, 2009, vol. 1, no. 2, p. 104-120. ISSN: 1741-8569.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). FIT-TR-2009-02, Brno: 2009. 29 p.Detail
IOSIF, R.; KONEČNÝ, F.; VOJNAR, T.; HABERMEHL, P.; BOZGA, M. Automatic Verification of Integer Array Programs. TR-2009-2, Grenoble: VERIMAG, 2009. 49 p.Detail
NOVOSAD, P.; ČEŠKA, M. Algorithms for Computing Coverability Graphs for Continuous Petri Nets. Proceedings of 22th European Simulation and Modelling Conference ESM'2008. EUROSIS-ETI Publications. Le Havre: EUROSIM-FRANCOSIM-ARGESIM, 2008. p. 489-491. ISBN: 978-90-77381-44-1.Detail
KŘENA, B.; LETKO, Z.; VOJNAR, T.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. Runtime Verification. Lecture Notes in Computer Science, Volume 5779/2009. Berlin: Springer Verlag, 2009. p. 101-114. ISBN: 978-3-642-04693-3.Detail
HABERMEHL, P.; VOJNAR, T. Proceedings of 10th International Workshop on Verification of Infinite-State Systems - INFINITY'08. Toronto: Faculty of Information Technology BUT, 2008. 74 p. ISBN: 978-80-214-3697-8.Detail
NOVOSAD, P.; ČEŠKA, M. Algorithms for Computing Coverability Graphs for Hybrid Petri Nets. 4th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Brno: Masaryk University, 2008. p. 177-183. ISBN: 978-80-7355-082-0.Detail
HÝSEK, J. Visual design of SmallDEVS models using statecharts. Proceedings of ASIS 2008. Rožnov pod Radhoštěm: Czech Science Foundation, 2008. p. 999-1004. ISBN: 978-80-86840-42-0.Detail
KOČÍ, R.; JANOUŠEK, V. System Design with Object Oriented Petri Nets Formalism. The Third International Conference on Software Engineering Advances Proceedings ICSEA 2008. Los Alamitos: IEEE Computer Society, 2008. p. 421-426. ISBN: 978-0-7695-3372-8.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; BOUAJJANI, A.; KAATI, L. Composed Bisimulation for Tree Automata. INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2009, vol. 20, no. 4, p. 685-700. ISSN: 0129-0541.Detail
DUDKA, V.; VOJNAR, T.; KŘENA, B. Self-healing Assurance using Bounded Model Checking. Computer Aided Systems Theory. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2009. p. 99-100. ISBN: 978-84-691-8502-5.Detail
ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. Pattern-Based Verification for Trees. Computer Aided Systems Theory - EUROCAST 2007. Las Palmas de Grand Canaria: The Universidad de Las Palmas de Gran Canaria, 2007. p. 181-182. ISBN: 978-3-540-75866-2.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; KAATI, L. A Uniform (Bi-)Simulation-Based Framework for Reducing Tree Automata. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, vol. 2009, no. 251, p. 27-48. ISSN: 1571-0661.Detail
KOČÍ, R.; JANOUŠEK, V. Towards Simulation-Based Design of the Software Systems. The Fourth International Conference on Software Engineering Advances. Los Alamitos: IEEE Computer Society, 2009. p. 452-457. ISBN: 978-1-4244-4779-4.Detail
HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y. Mediating for Reduction (On Minimizing Alternating Büchi Automata). IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009). LIPIcs, sv. 4. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2009. s. 1-12. ISBN: 978-3-939897-13-2.Detail
HABERMEHL, P.; IOSIF, R.; VOJNAR, T. A Logic of Singly Indexed Arrays. TR-2008-9, Grenoble: VERIMAG, 2008. 19 p.Detail
ERLEBACH, P.; ČEŠKA, M.; VOJNAR, T. Generalised Multi-Pattern-Based Verification of Programs with Linear Linked Structures. FORMAL ASPECTS OF COMPUTING, 2007, vol. 19, no. 3, p. 363-374. ISSN: 0934-5043.Detail
KOČÍ, R.; JANOUŠEK, V.; ZBOŘIL, F. Object Oriented Petri Nets -- Modelling Techniques Case Study. Second UKSIM European Symposium on Computer Modeling and Simulation. Liverpool: IEEE Computer Society, 2008. p. 165-170. ISBN: 978-0-7695-3325-4.Detail
HOLÍK, L.; ŠIMÁČEK, J. Optimizing an LTS-Simulation Algorithm. 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Znojmo: Faculty of Informatics MU, 2009. p. 93-101. ISBN: 978-3-939897-15-6.Detail
VOJNAR, T.; HABERMEHL, P.; BOUAJJANI, A. Verification of parametric concurrent systems with prioritised FIFO resource management. FORMAL METHODS IN SYSTEM DESIGN, 2008, vol. 32, no. 2, p. 129-172. ISSN: 0925-9856.Detail
IOSIF, R.; ROGALEWICZ, A. Automata-Based Termination Proofs. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 165-177. ISBN: 978-3-642-02978-3.Detail
HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. FIT-TR-2008-007, Brno: Faculty of Information Technology BUT, 2008. 15 p.Detail
ERLEBACH, P.; VOJNAR, T.; ČEŠKA, M. Pattern-based Verification for Trees. Computer Aided Systems Theory. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2007. p. 488-496. ISBN: 978-3-540-75866-2.Detail
HABERMEHL, P.; IOSIF, R.; ROGALEWICZ, A.; VOJNAR, T. Proving Termination of Tree Manipulating Programs. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2007. p. 145-161. ISBN: 978-3-540-75595-1.Detail
VOJNAR, T. Cut-offs and Automata in Formal Verification of Infinite-State Systems. FIT Monograph 1. FIT Monograph 1. Brno: Faculty of Information Technology BUT, 2007. 189 p. ISBN: 978-80-214-3547-6.Detail
HABERMEHL, P.; IOSIF, R.; VOJNAR, T. What else is decidable about integer arrays?. Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 475-490. ISBN: 978-3-540-78497-5.Detail
SMRČKA, A.: xx; Analyzátor CDC asynchronních komponent. xx. URL: http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreveal. (Software)Detail
DUDKA, V. Bounded Model Checking Using Java PathFinder. Proceedings of the 14th Conference STUDENT EEICT 2008. Volume 2. Brno: Brno University of Technology, 2008. p. 247-249. ISBN: 978-80-214-3615-2.Detail
KŘENA, B.; LETKO, Z.; TZOREF-BRILL, R.; UR, S.; VOJNAR, T. Healing Data Races On-The-Fly. Proceedings of 5th International Workshop on Parallel and Distributed Systems: Testing and Debugging Modelling - PADTAD'07. London: Association for Computing Machinery, 2007. p. 54-64. ISBN: 978-1-59593-734-6.Detail
LETKO, Z.; VOJNAR, T.; KŘENA, B.; NIR-BUCHBINDER, Y.; TZOREF-BRILL, R.; UR, S. A Concurrency Testing Tool and its Plug-ins for Dynamic Analysis and Runtime Healing. FIT-TR-2009-01, Brno: 2009. 15 p.Detail
KOČÍ, R.; JANOUŠEK, V.; ZBOŘIL, F. Object Oriented Petri Nets - Modelling Techniques Case Study. International Journal of Simulation Systems, Science & Technology, 2010, vol. 10, no. 3, p. 32-44. ISSN: 1473-8031.Detail
DUDKA, V.; KŘENA, B.; VOJNAR, T. Self-healing Assurance using Bounded Model Checking. Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2009. p. 295-303. ISBN: 978-3-642-04771-8.Detail
KOČÍ, R.; JANOUŠEK, V. Simulation Based Design of Control Systems Using DEVS and Petri Nets. Computer Aided Systems Theory - EUROCAST 2009. Lecture Notes in Computer Science, Volume 5717. Berlin: Springer Verlag, 2009. p. 849-856. ISBN: 978-3-642-04771-8.Detail
ZBOŘIL, F.; KOČÍ, R. Intention Structures Modelling Using Object Oriented Petri Nets. Proceedings of the 7th ISDA. Los Alamitos: IEEE Computer Society, 2007. p. 33-38. ISBN: 0-7695-2976-3.Detail
HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 57-67. ISBN: 978-3-540-70843-8.Detail
JANOUŠEK, V.; KOČÍ, R. Embedding Object-Oriented Petri Nets into a DEVS-based Simulation Framework. Proceedings of the 16th International Conference on System Science. volume 1. Wroclaw: Wroclaw University of Technology, 2007. p. 386-395. ISBN: 978-83-7493-339-1.Detail
KOČÍ, R.; JANOUŠEK, V. On the Dynamic Features of PNtalk. International Workshop on Petri Nets and Software Engineering 2009. Paříž: University of Pierre and Marie Curie, 2009. p. 189-206. Detail
JANOUŠEK, V.; KOČÍ, R. Simulation and Design of Systems with Object Oriented Petri Nets. Proceedings of the 6th EUROSIM Congress on Modelling and Simulation. Ljubljana: ARGE Simulation News, 2007. p. 1-9. ISBN: 978-3-901608-32-2.Detail
DUDKA, V.; KŘENA, B.; VOJNAR, T. Using JavaPathFinder for Self-healing Assurance. Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science - MEMICS 2007. Znojmo: Ing. Zdeněk Novotný, CSc., 2007. p. 67-73. ISBN: 978-80-7355-077-6.Detail
VOJNAR, T. Stromové automaty s omezeními v symbolické verifikaci programů manipulujících vyvážené stromy. Současné trendy teoretické informatiky. ITI Series 2007-347. Praha: 2007. s. 38-39. Detail
JANOUŠEK, V.; KVĚTOŇOVÁ, Š. On the Multilevel Petri Nets-Based Models in Project Engineering. International Workshop on Petri Nets and Software Engineering 2009. Paříž: University of Pierre and Marie Curie, 2009. p. 173-188. Detail
IOSIF, R.; VOJNAR, T.; HABERMEHL, P. Automata-based Verification of Programs with Tree Updates. ACTA INFORMATICA, 2010, vol. 47, no. 1, p. 1-31. ISSN: 0001-5903.Detail
LETKO, Z.; VOJNAR, T.; KŘENA, B. AtomRace: Data Race and Atomicity Violation Detector and Healer. PADTAD '08. Proceedings of the 6th workshop on Parallel and distributed systems. Seattle: Association for Computing Machinery, 2008. p. 1-10. ISBN: 978-1-60558-052-4.Detail
VOJNAR, T.; ČEŠKA, M.; ROGALEWICZ, A.; ERLEBACH, P.; HOLÍK, L.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T.; MORO, P. Automatická verifikace programů s dynamickými datovými strukturami. Inovační podnikání & transfer technologií, 2008, roč. 2008, č. 1, s. 21-22. ISSN: 1210-4612.Detail
Odpovědnost: Češka Milan, prof. RNDr., CSc.