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: Postdoktorandské granty
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
- RÁB, J.; RYŠAVÝ, O.; ŠVÉDA, M. On the Implementation of State-space Exploration Procedure in a Relational Database Management System. 30th IFAC Workshop on Real-Time Programming and 4th International Workshop on Real-Time Software. Mragowo: IEEE Computer Society, 2009.
p. 151-156. ISBN: 978-83-60810-22-4. Detail - RYŠAVÝ, O.; RÁB, J. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering, 2009, vol. 5, no. 2,
p. 139-149. ISSN: 1614-5046. Detail
2008
- RYŠAVÝ, O.; RÁB, J. A Component-based Approach to Verification of Embedded Control Systems using TLA. IEEE Proceedings of International Multiconference on Computer Science and Information Technology. Wisla: IEEE Computer Society Press, 2008.
p. 719-725. ISBN: 978-83-60810-14-9. Detail - ŠVÉDA, M.; RYŠAVÝ, O.; VRBA, R. Pattern-driven Reuse of Behavioral Specifications in Embedded Control System Design. In Frontiers in Robotics, Automation and Control. Vienna: IN-TECH Education and Publishing, 2008.
p. 151-164. ISBN: 978-953-7619-17-6. Detail
2007
- PETERKA, O.; RYŠAVÝ, O.; LORENC, V.; OSOVSKÝ, M.; ŠKARVADA, L. Can Objects Have Dependent Types?. Proceedings of 3rd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007). Znojmo: Ing. Zdeněk Novotný, CSc., 2007.
p. 173-180. ISBN: 978-80-7355-077-6. Detail - ŠVÉDA, M.; RYŠAVÝ, O. Industrial Application Development Using Case-Based Reasoning. Proceedings of International Workshop on Artificial Neural Networks and Intelligent Information Processing. Angers: Institute for Systems and Technologies of Information, Control and Communication, 2007.
p. 64-70. ISBN: 972-8865-86-4. Detail - ŠVÉDA, M.; VRBA, R.; RYŠAVÝ, O. Pattern-Driven Reuse of Embedded Control Design. Proceedings of Fourth International Conference on Informatics in Control, Automation and Robotics. Angers: Institute for Systems and Technologies of Information, Control and Communication, 2007.
p. 152-159. ISBN: 972-8865-84-8. Detail
2007
- Framework for the Deductive Analysis of Embedded Software: Initial technical report, výzkumná zpráva, 2007
Autoři: RYŠAVÝ, O.