Verification and Analysis of Large-Scale Computer Systems
| Description: |
The main objective of the project is to create a theoretical and methodological
base for computer-aided and automatic verification and analysis of large-scale computer
systems. The project aims to support the development of methodologies,
technologies and tools of software engineering in automatic and computer-aided
verification and analysis. 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 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.
|
| Identification: |
201/09/1389 |
| Funding: |
Grant Agency of the Czech Republic |
| Duration: |
2008–2010 |
| Publications: |
publications in MU database of publications |
| Investigator: |
Lubos Brim |
| Description: |
The main objective of the project is to create a theoretical and methodological
base for computer-aided and automatic 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.
|
| Identification: |
201/06/1338 |
| Funding: |
Grant Agency of the Czech Republic |
| Duration: |
2006–2008 |
| Publications: |
publications in MU database of publications |
| Investigator: |
Lubos Brim |
-->
| Description: |
The proposed project aims at development and analysis of new
original methods for effective verification of cocnurrent
systems. Main targets of the project can be summarized as
follows:
- Experimental environment for evaluation of verification
algorithms. In particular, tools for rapid implementation of new or
modified algorithms (e.g. in a distributed environment), their
integration, and comparison of their computational tractability will
be developed.
- Formal methods for computationally hard verification
problems. In particular, expressivelly restricted model languages
which allow for more effective verification algorithms will be
investigated (e.g. 1-safe Petri Nets, minimized non-deterministic
finite automata).
- Analyzis and development of new methods for
explicit and symbolic verification.
- Decomposition and
parallelization of selected verification problems.
|