"Muu" projekt BF99
BF99 "Formaalsed meetodid hajussüsteemides. (1.01.2009−31.12.2011)", Jüri Vain, Tallinna Tehnikaülikool, Tallinna Tehnikaülikool, Infotehnoloogia teaduskond, Arvutiteaduse instituut, Üldinformaatika õppetool.
BF99
Formaalsed meetodid hajussüsteemides.
Formal Methods in Distributed systems
Formaalsed meetodid hajussüsteemides.
1.01.2009
31.12.2011
Teadus- ja arendusprojekt
Muu
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
AsutusRiikTüüp
Tallinna Tehnikaülikool/ Tallinn University of Technology
PerioodSumma
01.01.2009−31.12.2011628 620,00 EEK (40 176,14 EUR)
40 176,14 EUR
HTM baasfinantseerimine

Projekti käigus luuakse meetodid robotparvede ja agentsüsteemide missiooni edukuse eelanalüüsiks. Missiooni edukuse üheks väljenduseks on hajuskoordinatsiooni algoritmide isestabiliseeruvus, mis seob saavutatavus- ja ohutusomadusi. Koordinatsiooni isestabiliseeruvus ei ole arvutusliku keerukuse tõttu tõestatav traditsiooniliste verifitseerimismeetoditega. Loodav lähenemine integreerib kompositsioonilise assume-guarantee tüüpi deduktiivse tõestusmeetodi mudelkontrolliga. Projekti töörühma poolt on väljatöötatud Williams-Nayaki reaktiivsel planeerimisel põhinev mittedeterministlike hajussüsteemide testimise meetod ja demonstreeritud selle eeliseid võrreldes teiste olemasolevate meetoditega. Projektis täiendatakse laiendatud lõplike automaadi (EFSM) esitust kasutavat meetodit ajaga automaatide (XTA) klassile ja lisatakse Dijkstra nõrgima eeltingimuse arvutusel põhinev testiandmete genereerimise meetod. Teoreetilised tulemused realiseeritakse projektide ELIKO2.2 ja D-Mint raames väljatöötatud testimiskeskkonna laiendusena. Formaalsete mudeliteoreetiliste verifitseerimis- ja planeerimismeetodite praktilise rakendamise üheks põhiprobleemiks on adekvaatse mudeli konstrueerimine. Koostöös Tokyo Denkiülikooli töörühmaga on projektis „Scrub Nurse Robot “ väljatöötatud sisend-väljund vaadeldava agentsüsteemi interaktsioonide õppimismeetod. Loodud õppimisalgoritmi, milles tulemusena genereeritakse ajaga automaatide kompositisoon, arendatakse edasi tõenäosuslikele ajaga automaatidele. Mudelis esitatavad vaatlustel tuginevad tõenäosushinnangud võimaldavad vähendada mittetäielikest vaatlusandmetest põhjustatud määramatust ja suurendavad planeerimisotsustuste usaldusväärsust. Loodava õppimisalgoritmi rakendusteks on konteksti tuvastus ja käitumisega seotud kasutajaprofiilide õppimine veebisüsteemides, samuti inimesele kohanduva assistent-roboti plaanur.
Within the project the formal methods for feasibility evaluation of robot swarms’ and agent systems’ missions are developed. The feasibility of mission is defined in terms of self-stabilization property of distributed coordination algorithms used in those systems. The self-stabilization properties combining reachability and safety are not efficiently decidably using traditional verification methods because of high complexity of real systems. The verificatiton method to be created integrates assume-guaranee type resoning with symbolic model checking. The project team has created a model-based test generation technique – rective planning tester synthesis method (RPTS) for non-deterministic systems. The method extends Williams-Nayak reactive planning principle and has demonstrated its superiority over other alternative techniques. In this project the RPTS technique is extended from EFSM to Uppaal timed automata and data dependencies are included using Dijkstra’s wp-calculus. Theoretical results are implemented within ELIKO2.2 and D-Mint projects. A key issue of fomal model-based verfication and planning methods is model construction. In cooperation with Tokyo Denki University the timed automata learning method is developed. In this project the method will be developed further for learning probabilistic timed automata (PTA). The probability estimates represented in the PTA model allow to reduce uncertainty of non-deterministic choices and increase trustabiity of model-based planning. The learning algoritm has applications for user profile recognition in customized web-service systems and in action planning systems of human-addaptive robots.
KirjeldusProtsent
Alusuuring60,0
Rakendusuuring40,0