Project information
Realistic application of formal methods in component systems
- Project Identification
- 1ET400300504
- Project Period
- 1/2005 - 12/2009
- Investor / Pogramme / Project type
-
Academy of Sciences of the Czech Republic
- Information society (National programme of research)
- MU Faculty or unit
- Faculty of Informatics
- Keywords
- formal verification, behavior description, software components, component systems
- Cooperating Organization
-
Institute of Computer Science of the ASCR, v. v. i.
- Responsible person prof. Ing. František Plášil, DrSc.
- Responsible person prof. Ing. Petr Tůma, Dr.
The project supports component-based application development by combining components with formal behavior description and by designing tools for automated checking of the architecture of applications composed of components with formal behavior description. The project aims to design and implement a functional prototype of a platform for formal verification of component applications using this platform. The platform will be open to the emerging methods of formal verification and code analysis, and used to test the suitability and applicability of these methods, especially with respect to model checking. The work on the formal verification methods will focus on identifying approaches to make the existing verification tools more efficient, especially in a distributed environment.
Results
Publications
Total number of publications: 29
2008
-
Automated Computing of the Maximal Number of Handled Clients for Client-Server Systems
Proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08), year: 2008
-
Component-Interaction Automata Approach (CoIn)
The Common Component Modeling Example: Comparing Software Component Models, year: 2008, number of pages: 31 s.
-
Formal verification of systems with an unlimited number of components
IET Software journal, year: 2008, volume: Volume 2, edition: Isuue 6
-
Model Checking of Control-User Component-Based Parametrised Systems
Year: 2008, type: R&D Presentation
-
Model Checking of Control-User Component-Based Parametrised Systems
Lecture Notes in Computer Science 5282, year: 2008
-
Modelling and Formal Analysis of Component-Based Systems in View of Component Interaction
Year: 2008, type: R&D Presentation
-
Partial Order Reduction for State/Event LTL
Year: 2008
-
Revisiting Resistance Speeds Up I/O Efficient LTL Model Checking
Tools and Algorithms for the Construction and Analysis of Systems, year: 2008
-
The CoIn Tool: Modelling and Verification of Interactions in Component-Based Systems
Pre-proceedings of the International Workshop on Formal Aspects of Component Software (FACS'08), year: 2008
2007
-
Component Substitutability via Equivalencies of Component-Interaction Automata
Electronic Notes in Theoretical Computer Science, year: 2007, volume: 182, edition: 1