| title: | Abstraction-based verification and analysis of infinite state systems |
|---|---|
| reg no: | ETF5775 |
| project type: | Estonian Science Foundation research grant |
| subject: |
2.9. System Engineering and Computer Technology |
| status: | accepted |
| institution: | Institute of Cybernetics at Tallinn Technical University |
| head of project: | Jüri Vain |
| duration: | 01.01.2004 - 31.12.2007 |
| description: | The aim of this project is to elaborate a new abstraction-based verification method for proving design correctness of systems with hybrid dynamics. Present verification methods are effective mainly when applied to systems with finite state space and for proving state properties. Temporal reasoning of infinite state systems is weakly scalable. Still, it is know that the scalability of present methods can be improved by using heuristics (e.g., application dependent verification strategies), compositional verification and appropriate abstraction techniques. The approach used in this proposal is innovative in the sense that the general abstraction aided verification methodology developed by A.Pnueli (so called AAV methodology) is instantiated using the theory of o-minimal structures of real numbers. That gives the well founded basis for constructing finitary abstractions of systems with hybrid (continuous and discrete) state spaces. This abstraction method is planned to implement in the first order theorem prover Gandalf and as an extension to existing model checking systems SMV and Uppaal (cooperation with University of Aalborg, Denmark). |
| project group | ||||
|---|---|---|---|---|
| no | name | institution | position | |
| 1. | Juhan-Peep Ernits | TTÜ KI | ||
| 2. | Marko Kääramees | TTÜ KI | teadur | |
| 3. | Tanel Tammet | Tallinn Technical University | professor | |
| 4. | Jüri Vain | Institute of Cybernetics at Tallinn Technical University | Head of Dept. | |