Project Details
Framework for the deductive analysis of embedded software
Project Period: 1. 1. 2007 – 31. 12. 2008
Project Type: grant
Code: GP201/07/P544
Agency: Czech Science Foundation
Program: Postdoktorandské granty
Embedded Systems, Domain Specific Languages, Logical Framework, Formal program
development, Formal Specification, Formal Verification
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.
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