Detail projektu
Framework for the deductive analysis of embedded software
Období řešení: 1. 1. 2007 - 31. 12. 2008
Typ projektu: grant
Kód: GP201/07/P544
Agentura: Grantová agentura České republiky
Program:
Vestavěné systémy, Doménově specifické jazyky, Formální vývoj programů, Formální specifikace, Formální verifikace
Navrhovaný projekt představuje základní výzkum v problematice integrace formálních metod a doménově specifikačních jazyků pro návrh vestavěných systémů. Uvažované řešení bude založeno na definici formálního rámce disponujícího deduktivním odvozovacím aparátem pro interpretaci a ověřování vlastností doménově
specifických modelů. Formální rámec poskytne také prostředí pro integraci automatických verifikačních method pro ověřování vlastností modelovaných systémů. Cílem uvažovaného řešení je navržení doménově specifického modelovacího jazyka s definovanou formální sémantiku a demonstrace možnosti kombinace deduktivní a automatické verifikace pro ověřování takto specifikovaných systémů. Použití formálního rámce přináší možnost ověření korektnosti extrakce specifikace z doménového specifického modelovacího jazyka a transformace pro jednotlivé verifikační nástroje.
2009
- RYŠAVÝ Ondřej a RÁB Jaroslav. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering, roč. 5, č. 2, 2009, s. 139-149. ISSN 1614-5046. Detail
- RÁB Jaroslav, RYŠAVÝ Ondřej a ŠVÉDA Miroslav. On the Implementation of State-space Exploration Procedure in a Relational Database Management System. In: 30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software. Mragowo: IEEE Computer Society, 2009, s. 151-156. ISBN 978-83-60810-22-4. Detail
2008
- RYŠAVÝ Ondřej a RÁB Jaroslav. A Component-based Approach to Verification of Embedded Control Systems using TLA. In: IEEE Proceedings of International Multiconference on Computer Science and Information Technology. Wisla: IEEE Computer Society Press, 2008, s. 719-725. ISBN 978-83-60810-14-9. Detail
- ŠVÉDA Miroslav, RYŠAVÝ Ondřej a VRBA Radimír. Pattern-driven Reuse of Behavioral Specifications in Embedded Control System Design. Frontiers in Robotics, Automation and Control. Vienna: IN-TECH Education and Publishing, 2008, s. 151-164. ISBN 978-953-7619-17-6. Detail
2007
- PETERKA Ondřej, RYŠAVÝ Ondřej, LORENC Václav, OSOVSKÝ Martin a ŠKARVADA Libor. Can Objects Have Dependent Types?. In: Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo: Ing. Zdeněk Novotný, CSc., 2007, s. 173-180. ISBN 978-80-7355-077-6. Detail
- ŠVÉDA Miroslav a RYŠAVÝ Ondřej. Industrial Application Development Using Case-Based Reasoning. In: Proceedings of International Workshop on Artificial Neural Networks and Intelligent Information Processing. Angers: Institute for Systems and Technologies of Information, Control and Communication, 2007, s. 7. ISBN 972-8865-86-4. Detail
- ŠVÉDA Miroslav, VRBA Radimír a RYŠAVÝ Ondřej. Pattern-Driven Reuse of Embedded Control Design. In: Proceedings of Fourth International Conference on Informatics in Control, Automation and Robotics. Angers: Institute for Systems and Technologies of Information, Control and Communication, 2007, s. 8. ISBN 972-8865-84-8. Detail