Detail projektu

Framework for the deductive analysis of embedded software

Období řešení: 01.01.2007 — 31.12.2008

Zdroje financování

Grantová agentura České republiky - Postdoktorandské granty

- plně financující (2007-01-01 - 2008-12-31)

O projektu

The proposed project aims at basic research in the area of possible support of formal methods for domain specific modeling languages (DSML) for embedded systems by means of designing a formal verification framework based on a deductive verification tool. Formal framework provides the common logical foundation for the representation of DSML semantics and for interpretation of languages of verification tools that can be used for checking the properties of modeled systems. The purpose of common foundation is to guarantee the correctness of application of verification tools as the correctness of transformations and mappings from the DSML to particular languages of verification tools can be formally proved.

Popis česky
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.

Klíčová slova
Embedded Systems, Domain Specific Languages, Logical Framework, Formal program development, Formal Specification, Formal Verification

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

Označení

GP201/07/P544

Originální jazyk

angličtina

Řešitelé

Ryšavý Ondřej, doc. Ing., Ph.D. - hlavní řešitel

Útvary

Ústav informačních systémů
- spolupříjemce (01.01.2007 - 31.12.2008)

Výsledky

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

RYŠAVÝ, O. Framework for the Deductive Analysis of Embedded Software: Initial technical report. Brno: Department of Information Systems FIT BUT, 2007.
Detail

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

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

Š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

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

Odkaz

http://www.fit.vutbr.cz/~rysavy/projects/aves/pmwiki.php?n=Project.GACRP544

Odpovědnost: Ryšavý Ondřej, doc. Ing., Ph.D.