Framework for the deductive analysis of embedded software

Název česky

Rámec pro deduktivní analýzu softwarových aplikací vestavěných systémů

Typ

grant

Klíčová slova

Vestavěné systémy, Doménově specifické jazyky, Formální vývoj programů, Formální specifikace, Formální verifikace

Abstrakt

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.

Řešitelé

Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT) , hlavní řešitel

Publikace

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