Framework for the deductive analysis of embedded software

Czech title

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

Type

grant

Keywords

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

Abstract

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.

Team members

Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT) , research leader

Publications

2009

RYŠAVÝ Ondřej and RÁB Jaroslav. A Formal Model of Composing Components: The TLA+ Approach. Innovations in Systems and Software Engineering, vol. 5, no. 2, 2009, pp. 139-149. ISSN 1614-5046. Detail
RÁB Jaroslav, RYŠAVÝ Ondřej and Š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, pp. 151-156. ISBN 978-83-60810-22-4. Detail

2008

RYŠAVÝ Ondřej and 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, pp. 719-725. ISBN 978-83-60810-14-9. Detail
ŠVÉDA Miroslav, RYŠAVÝ Ondřej and 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, pp. 151-164. ISBN 978-953-7619-17-6. Detail

2007

PETERKA Ondřej, RYŠAVÝ Ondřej, LORENC Václav, OSOVSKÝ Martin and Š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, pp. 173-180. ISBN 978-80-7355-077-6. Detail
ŠVÉDA Miroslav and 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, p. 7. ISBN 972-8865-86-4. Detail
ŠVÉDA Miroslav, VRBA Radimír and 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, p. 8. ISBN 972-8865-84-8. Detail