Testitapausten generointi muodollisten spesifikaatioiden perusteella

Quality is a persistent problem in software development. The main method for quality assurance, testing, is a significant part of any software project. As software development processes move towards continuous integration and deployment, there is demand to increase the level of automation in testing. Conventionally, test automation refers to automating the execution of tests. However, the test cases are written one-by-one, which can get very repetitive. This is also more costly, especially in the maintenance phase. An alternative to these example-based tests are property-based tests, where properties define sets of tests at once. In other words test cases are generated from these properties. Testing targets a certain interface, such as a class, an HTTP API or a GUI. A set of properties – a formal specification – describes the desired behavior of the interface. There is always a human element to specification, because correctness largely depends on the situation and is often subjective. However, verifying that a system adheres to that specification can be automated, at least to some extent. Test case generation is mostly used in functional programming, but this thesis explores it in the object-oriented paradigm as well. Other means of verification are also discussed, and central theoretical concepts are covered. A case study is described, where test cases were generated for the M-Files API – an object-oriented .NET API.Ohjelmiston laatu on ongelma, joka tuskin tulee katoamaan. Laadunvarmistus tapahtuu pääosin testaamalla, ja se on merkittävä osa mitä tahansa ohjelmistoprojektia. Modernit ohjelmistokehitysprosessit perustuvat jatkuvalle integraatiolle ja käyttöönotolle, mikä vaatii testaukselta korkeampaa automaatiotasoa. Perinteisesti testiautomaatio viittaa testien automaattiseen suoritukseen. Tällöin automaatiotasossa on kuitenkin parannettavaa, sillä testien kirjoittaminen voi olla hyvinkin mekaanista toistoa. Tämä taas tulee kalliiksi etenkin ohjelmiston ylläpitovaiheessa. Perinteisten esimerkkipohjaisten testien vaihtoehto on ominaisuuspohjainen testaus, jossa yksittäisten testien sijaan määritellään testijoukkoja. Toisin sanoen ominaisuudet toimivat testitapauksien generoinnin lähtökohtana. Testaamisen kohteena on aina jokin rajapinta, kuten luokka, HTTP API tai graafinen käyttöliittymä. Ominaisuuksien joukko – muodollinen spesifikaatio – kuvailee rajapinnan haluttua toimintaa. Spesifikaation määrittelyssä on aina inhimillinen osuus, sillä järjestelmän virheettömyys on aina paljolti subjektiivista. Sen varmistaminen, että järjestelmä vastaa jotain tiettyä muodollista spesifikaatiota, on kuitenkin yleensä mahdollista automatisoida, ainakin jossain määrin. Testitapausten generoinnin hyödyntäminen on yleisimmillään funktionaalisessa ohjelmoinnissa, mutta tässä työssä sitä tarkastellaan myös olio-ohjelmoinnin yhteydessä. Muitakin verifiointimenetelmiä käsitellään lyhyesti, sekä keskeiset teoreettiset käsitteet käydään läpi. Lisäksi esimerkkitapauksena tutkitaan testien generointia M-Files API:lle, joka on oliopainotteinen .NET-rajapinta