Project information
Techniques for automatic verification and validation of software nad hardware systems
- Project Identification
- 1ET408050503
- 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
- Computer aided and automatic verication, theory and technology of modellingof large systems, methodology of software engineering, embedded systems, parallel and distributed systems, real time systems.
The main objective of the project is to create a theoretical and methodological base for computer-aided and automatic verification and validation of large software and hardware 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 large systems, including real-time systems and probabilistic 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
Publications
Total number of publications: 94
2008
-
A Case Study in Parallel Verification of Component-Based Systems
Electronic Notes in Theoretical Computer Science, year: 2008, volume: 220, edition: 2
-
A Case Study in Parallel Verification of Component-Based Systems
Pre-proceedings of the Workshop on Parallel and Distributed Methods in verifiCation (PDMC'08), year: 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
-
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
-
Formal verification of systems with an unlimited number of components
IET Software journal, year: 2008, volume: Volume 2, edition: Isuue 6
-
From Simple Regulatory Motifs to Parallel Model Checking of Complex Transcriptional Networks
Proceedings of PDMC 2008 - Parallel and Distributed Methods ins VerifiCation, year: 2008