See veebileht kasutab küpsiseid kasutaja sessiooni andmete hoidmiseks. Veebilehe kasutamisega nõustute ETISe kasutustingimustega. Loe rohkem
Olen nõus
"Institutsionaalne uurimistoetus (IUT)" projekt IUT33-13
IUT33-13 "Tugevate garantiidega tarkvara meetodid, tööriistad ja protsessid (1.01.2015−31.12.2020)", Tarmo Uustalu, Tallinna Tehnikaülikool, TTÜ Küberneetika Instituut, Tallinna Tehnikaülikool, Infotehnoloogia teaduskond, Tarkvarateaduse instituut.
IUT33-13
Tugevate garantiidega tarkvara meetodid, tööriistad ja protsessid
Methods, tools and processes for software with strong guarantees
1.01.2015
31.12.2020
Teadus- ja arendusprojekt
Institutsionaalne uurimistoetus (IUT)
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
PerioodSumma
01.01.2015−31.12.2015180 000,00 EUR
01.01.2016−31.12.2016180 000,00 EUR
01.01.2017−31.12.2017180 000,00 EUR
01.01.2018−31.12.2018180 000,00 EUR
01.01.2019−31.12.2019180 000,00 EUR
01.01.2020−31.12.2020180 000,00 EUR
1 080 000,00 EUR

Käesolevas IUTs edendame tarkvara usaldusväärsuse garanteerimise meetodeid, tööriistu ja protsesse. Arendame sõltuvalt tüübitud programmeerimist (DTP) kui funktsionaalprogrammeerimise variatsiooni, kus koodi korrektsuse tagab tüübikontroll programme detailselt spetsifitseerivate tüüpide suhtes kombineerituna interaktiivse teoreemitõestamisega. Arendame matemaatiliselt motiveeritud abstraktsioone efektidega ja kontekstist sõltuvaks arvutamiseks, andmestruktuuride töötlemiseks, reaktiivseks arvutamiseks funktsionaalprogrammeerimises ja DTPs. Uurime uusi suundi olekumasinate ja rakuautomaatide kui äärmiselt laia rakendusalaga abstraktsete arvutusmudelite teoorias. Disainime uudseid tüübisüsteeme ja programmiloogikaid interaktsiooni ja konkurentsuse jaoks, formaliseerime nende metateooria. Edendame ajaga reaktiivsete süsteemide mudelipõhise testimise teooriat ja praktikat. Samuti arendame semantilise veebi tehnoloogiaid rakendusteks Eesti IT-süsteemide juures.
In this institutional research theme we will advance methods, tools and processes for guaranteeing trustworthiness of software. We will work on dependently typed programming as an elaboration of functional programming where correctness of code is established by type-checking against detailed types-as-specifications aided by interactive theorem-proving. We will develop mathematically motivated programming abstractions for effectful and context-dependent computation, datastructure manipulation, reactive computation in functional programming and DTP. We will pursue new directions in the theory of state machines and cellular automata as abstract models of computation with very wide applicability. We will devise novel type systems and program logics for interaction and concurrency, formalize their metatheory. We will develop the theory and practice of model-based testing of timed reactive systems. We will also develop semantic web technologies for applications in Estonian IT systems.
Arendasime meetodeid, tööriistu ja protsesse tarkvara usaldusväärsuse tõstmiseks. Eelkõige puudutavad need programmeerimiskeeli ning tarkvara analüüsi ja konstrueerimise tööriistu, mis on sihitud tarkvaraarenduse muutmisele vähem vea-altiks ja efektiivsemaks, saavutamaks parema kvaliteediga tarkvara, millel on tugevad garantiid. Keeledisaini ja semantika tasemel edendasime arvutuslike efektidega funktsionaalprogrammeerimist ja sõltuvate tüüpidega programmeerimist, mis on tähtsad uued programmeerimise paradigmad. Saavutasime rea uusi tulemusi olekumasinate ja rakuautomaatide kohta, mis on väga laia kasutusalaga mudelid vastavalt olekupõhiseks arvutamiseks ja hajusarvutamiseks homogeensel võrel. Edendasime tarkvara testimise mudelipõhiseid meetodeid rakendustega robootikas ja meresõiduohutuses. Arendasime ontoloogiapõhiseid infosüsteemide disaini meetodeid ja kasutasime neid praktilistes rakendustes.