Project information
Automated software verification
- Project Identification
- GA201/06/1338
- Project Period
- 1/2006 - 12/2008
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
- Keywords
- verification, model-checking, software, components
The main objective of the project is to create a theoretical and methodological base for computer-aided and autotic verification and validation of software systems. The project aims to support the development of methodologies, technologies and tools of software engineering in automatic and computer-aided verification. The project is to contribute to the research into new technologies for a realistic modelling of software systems, including real-time systems, especially with respect to their safety. The aim is to design effective implementations of these models as well as efficient verification technologies based on such models. The project will focus on embedded distributed and parallel systems. Taking into consideration the complexity of verification processes the aim is to design methodologies that will make the maximum possible use of new information technologies, such as parallel and distributed computing and hierarchical memories.
Results
The main objective of the project is to create a theoretical and methodological base for computer-aided and autotic verification and validation of software systems.
Publications
Total number of publications: 45
2011
-
Flash memory efficient LTL model checking
Science of Computer Programming, year: 2011, volume: 76, edition: 2, DOI
2009
-
Can Flash Memory Help in Model Checking?
Formal Methods for Industrial Critical Systems, year: 2009
-
Local Quantitative LTL Model Checking
Formal Methods for Industrial Critical Systems, year: 2009
-
On Decidability of LTL Model Checking for Process Rewrite Systems
Acta informatica, year: 2009, volume: 46, edition: 1
2008
-
Can Flash Memory Help in Model Checking?
13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008), year: 2008
-
Component-Interaction Automata Approach (CoIn)
The Common Component Modeling Example: Comparing Software Component Models, year: 2008, number of pages: 31 s.
-
DiVinE Cluster
Year: 2008
-
DiVinE Multi-Core -- A Parallel LTL Model-Checker
Automated Technology for Verification and Analysis, year: 2008
-
Estimating State Space Parameters
Year: 2008, type: Appeared in Conference without Proceedings
-
I/O Efficient Model Checking
Year: 2008, type: Appeared in Conference without Proceedings