"Eesti Teadusfondi uurimistoetus" projekt ETF5775
ETF5775 (ETF5775) "Lõpmatu olekuruumiga süsteemide abstraktsiooni-põhine verifitseerimine ja analüüs (1.01.2004−31.12.2007)", Jüri Vain, Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut.
ETF5775
Lõpmatu olekuruumiga süsteemide abstraktsiooni-põhine verifitseerimine ja analüüs
Abstraction-based verification and analysis of infinite state systems
1.01.2004
31.12.2007
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.7. Info- ja kommunikatsioonitehnoloogiaT181 Kaugseire2.2. Elektroenergeetika, elektroonika (elektroenergeetika, elektroonika, sidetehnika, arvutitehnika ja teised seotud teadused)100,0
PerioodSumma
01.01.2004−31.12.2004115 000,00 EEK (7 349,84 EUR)
01.01.2005−31.12.2005110 588,24 EEK (7 067,88 EUR)
01.01.2006−31.12.2006112 800,00 EEK (7 209,23 EUR)
01.01.2007−31.12.2007112 800,00 EEK (7 209,23 EUR)
28 836,18 EUR

Projekti eesmärgiks on uue abstraktsiooni-põhise verifitseerimismeetodi väljatöötamine hübriidse dünaamikaga süsteemide disaini korrektsuse tõestamiseks. Senised verifitseerimismeetodid on efektiivsed vaid lõpliku olekuruumiga süsteemide olekuomaduste tõestamisel. On teada, et olemasolevate meetodite skaleeruvust saab parandada heuristiliste verifitseerimisstrateegiate, kompositsioonilise tõestamise ja abstraktsioonide abil. Käesolev lähenemine on uudne selle poolest, et A.Pnueli poolt pakutud üldist abstraktsiooni-põhist verifitseerimismetoodikat (nn AAV metoodikat) konkretiseeritakse kasutades reaalarvude o-minimaalsete struktuuride teooriat. Viimane annab põhjendatud teoreetilise aluse lõplike abstraktsioonide konstrueerimiseks ka kontinuumi võimsusega olekuruumiga süsteemide korral. Loodav abstraktsiooni meetod on kavas realiseerida teoreemitõestuskeskkonnas Gandalf ja olemasolevate mudelkontrollijate SMV ning Uppaal laiendustena (koostöö Aalborgi Ülikooli töörühmaga).
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).