ɫɫÀ²

Tapahtumat

Väitös automaation ja säätötekniikan alalta, DI Antti Pakonen

Väitös Aalto-yliopiston sähkötekniikan korkeakoulusta, sähkötekniikan ja automaation laitokselta
Kuvitus puhujakorokkeesta ja sen yläpuolella olevasta tohtorinhatusta.

Väitöskirjan nimi: Practical solutions for the model-checking of fault-tolerant instrumentation and control system logics

³Õä¾±³Ù³Ù±ð±ô¾±Âáä: Antti Pakonen
³Õ²¹²õ³Ù²¹±¹Ã¤¾±³Ù³ÙäÂáä:&²Ô²ú²õ±è;Prof. Alexandre Philippot, l’Université de Reims Champagne-Ardenne (URCA), Ranska
Kustos: Prof. Valeriy Vyatkin, Aalto-yliopiston sähkötekniikan korkeakoulu

Yhteiskunnan kannalta kriittisiäkin prosesseja ohjaavat automaatiojärjestelmät ovat nykyään ohjelmistopohjaisia. Perinteisesti automaatio-ohjelmistojen virheettömyys on pyritty todentamaan esim. testaamalla, mutta ohjelmistojen monimutkaisuuden vuoksi täydellistä testikattavuutta ei useimmiten voida saavuttaa. Erityisen vaikeaa on todentaa, ettei järjestelmä tee jotain ei-toivottua. 

Mallintarkastus (eng. model checking) on tietokoneavusteinen menetelmä, jonka avulla voidaan loogisesti todistaa, että järjestelmästä tehty malli täyttää annetut vaatimukset. VTT on löytynyt mallintarkastuksen avulla yhteensä jo yli sata suunnitteluvirhettä suomalaisten ydinvoimalaitosten ja raideliikennejärjestelmien automaatio-ohjelmistoista. Piileviä virheitä on löytynyt senkin jälkeen, kun järjestelmiä oli jo perusteellisesti testattu. 

Väitöskirjassani olen tutkinut keinoja tehdä automaatio-ohjelmistojen mallintarkastuksesta helpompaa, käytännöllisempää ja halvempaa. Lisäksi olen löytänyt uusia keinoja soveltaa mallintarkastusta entistä laajemmin. Esitän keinoja huomioida ohjelmiston tarkastuksessa automaatiolaitteiden vikaantumistapoja. Näytän, kuinka reaalilukumatematiikkaan perustuvia algoritmeja ja osissa todentamisen menetelmiä voidaan soveltaa malleihin, joita laajemmin käytetyt (äärellisiin tilakoneisiin ja symboliseen todennukseen perustuvat) mallintarkastimet eivät pysty käsittelemään. 

Työssä tutkitut uudet tekniikat on jo otettu käyttöön VTT:n projekteissa, ja niiden avulla on jo paljastunut suunnitteluvirheitä ohjelmistomalleissa, joita aiemmin käytetyillä tekniikoilla ei ollut mahdollista tarkastaa.

Linkki väitöskirjan sähköiseen esittelykappaleeseen (esillä 10 päivää ennen väitöstä):  

Yhteystiedot:
antti.pakonen@vtt.fi
040 129 2785

Sähkötekniikan korkeakoulun väitöskirjat

Suuri valkoinen 'A!' veistos Otaniemen Kandidaattikeskuksen katolla. Taustalla puu ja muita rakennuksia.

Sähkötekniikan korkeakoulun väitöskirjat ovat saatavilla yliopiston ylläpitämässä avoimessa Aaltodoc-julkaisuarkistossa.

Zoom pikaopas
  • ±Êä¾±±¹¾±³Ù±ð³Ù³Ù²â:
  • Julkaistu:
Jaa
URL kopioitu