Project detail

Framework for the deductive analysis of embedded software

Duration: 01.01.2007 — 31.12.2008

Funding resources

Czech Science Foundation - Postdoktorandské granty

- whole funder (2007-01-01 - 2008-12-31)

On the project

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.

Description in Czech
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.

Keywords
Embedded Systems, Domain Specific Languages, Logical Framework, Formal program development, Formal Specification, Formal Verification

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

Mark

GP201/07/P544

Default language

English

People responsible

Ryšavý Ondřej, doc. Ing., Ph.D. - principal person responsible

Units

Department of Information Systems
- co-beneficiary (2007-01-01 - 2008-12-31)

Results

PETERKA, O.; RYŠAVÝ, O.; LORENC, V.; OSOVSKÝ, M.; ŠKARVADA, L. 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. p. 173-180. ISBN: 978-80-7355-077-6.
Detail

ŠVÉDA, M.; RYŠAVÝ, O. 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. p. 64-70. ISBN: 972-8865-86-4.
Detail

ŠVÉDA, M.; VRBA, R.; RYŠAVÝ, O. 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. 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

Link

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

Responsibility: Ryšavý Ondřej, doc. Ing., Ph.D.