Vaatimusten verifiointi simulaatiopohjaisessa automaatiotestauksessa

An important question in planning automation of industrial processes is whether or not it satisfies requirements imposed on it. The emergence of industrial internet combined with advanced control solutions has increased the number of cyber-physical connections between the system to be controlled and its automation. This has introduced new, complex dependencies to the system and thus made it harder to check whether the system satisfies its requirements. New advanced simulation-based design methodologies have made it possible to find find requirement violations before the actual physical system exists. Requirement verification consists of two problems: how to formalize the requirements in an unambiguous way, and how to check whether or not the system satisfies all requirements. An algorithm used in conventional software testing, which monitors a single simulation run and outputs whether or not a requirement formalized with an unambiguous language called Metric Temporal Logic is modified and implemented in this master's thesis. A case study where the algorithm implementation is used on the requirements imposed on a automation of a real industrial process is then conducted to test the algorithm and tool build around it. The results of the case study show that the algorithm and the tool built around it work well and that Metric Temporal Logic can be used to formalize requirements typical for at least some kind of automation systems. However, the case study also reveals a problem related to specific kind of requirements. At the end of the thesis, a possible solution to this problem is presented and extending of the algorithm with this solution is proposed as a topic for further research.Kun suunnitellaan teollisuuden prosessien automaatiojärjestelmiä, tärkeä kysymys on, täyttävätkö ne niille asetetut vaatimukset. Teollisen internetin synty yhdistettynä edistyneisiin säätöteknisiin ratkaisuihin on lisännyt automaation ja säädettävien prosessien välisiä liitäntöjä. Samalla on syntynyt uusia, monimutkaisia systeemin sisäisiä riippuvuuksia ja siten systeemin vaatimustenmukaisuuden tarkastamisesta on tullut vaikeampaa. Uudet kehittyneet simulaatiopohjaiset suunnittelumenetelmät ovat tehneet mahdolliseksi sen, että vaatimusrikkomukset on mahdollista löytää ennen fyysisen järjestelmän rakentamista. Vaatimusten verifiointi koostuu kahdesta osasta: kuinka vaatimukset formalisoidaan, eli ilmaistaan yksiselitteisesti, ja kuinka varmistetaan että järjestelmä täyttää sille asetetut formalisoidut vaatimukset. Tässä diplomityössä käytetään muunneltua versiota perinteisessä tietokoneohjelmien testauksessa käytetystä algoritmista. Algoritmi monitoroi yksittäistä simulaatiosuoritusta ja ilmoittaa, täyttääkö se halutut metrisellä temporaalilogiikalla formalisoidut vaatimukset. Lisäksi algoritmia ja sen ympärille rakennettua työkalua testataan tapaustutkimuksessa oikean teollisen prosessin automaation vaatimuksiin. Tapaustutkimuksesta saatujen tulosten perusteella algoritmi ja työkalu toimivat hyvin. Lisäksi metrinen temporaalilogiikka soveltuu tulosten perusteella ainakin joidenkin automaatiojärjestelmien vaatimusten formalisointiin. Tämän lisäksi tapaustutkimuksen perusteella algoritmilla on vaikeuksia verifioida tietyn tyyppisiä vaatimuksia. Diplomityön lupssa esitetään mahdollinen ratkaisu ongelman poistamiseksi ja algoritmin laajentamista ratkaisun osoittamalla tavalla ehdotetaan mahdolliseksi aiheeksi jatkotutkimukselle