Toiminnallinen verifiointi prosessiautomaatiossa

Tutkimuksessa tarkastellaan automatiikkojen, erityisesti ohjaussekvenssien toiminnallista verifiointia. Esitettävän menetelmän perusajatus on kuvata samalla formalismilla sekä automatiikan toiminnallinen määrittely että ohjattavan laitoksen toiminnalliset ominaisuudet ja tarkistaa, että näin saatu kokonaisjärjestelmän kuvaus vastaa toiminnallisilta ominaisuuksiltaan annettuja vaatimuksia. Ohjattavan laitoksen jatkuva-aikaisten ilmiöiden kuvaamiseen on sovellettu ns. kvalitatiivista mallitueta. Raportin pääpaino on prosessien ja ohjauslogiikan mallinnuksessa. Toiminnan oikeellisuutta on tarkistettu toisaalta yksinkertaisella ohjelmalla, joka generoi järjestelmän saavutettavuusgraafin, toisaalta pyrkimällä visualisoimaan järjestelmän toimintaa. Esimerkeissä käytetty ohjelmisto on toteutettu Prolog-ohjelmointikielellä, jolla on myös kuvattu tarkasteltavat järjestelmät. Raportin perustarkoitus on tarkastella prosessilaitoksen ohjausongelmaa, korostaa tapahtumapohjaisen ohjauksen osuutta ja esitellä erästä tietämystekniikan tarjoamaa mahdollisuutta tukea tapahtumapohjaisen ohjauksen suunnittelua