| kirjeldus: |
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). |