Tämän opinnäytetyön tarkoitus on selvittää niitä periaatteita ja tekniikoita, joiden avulla voidaan tarkistaa ohjelmistokomponenttien välinen yhteentoimivuus. Yhteentoimivuuden tarkistamista tarvitaan komponenttien uudelleenkäytön mahdollistamiseksi sekä ohjelmistoarkkitehtuurien suunnittelun yhteydessä.
Ohjelmistokomponentin yhteentoimivuus muiden komponenttien kanssa riippuu sen syntaktisista ja semanttisista ominaisuuksista sekä ulkoisesta käyttäytymisestä. Nämä ominaisuudet määritellään formaalisti tyyppiteoriaa, ontologioita ja prosessialgebroja käyttäen. Komponenttien syntaktinen korvautuvuus määritellään niin kutsuttujen termiautomaattien ja niiden välisten suhteiden avulla. Komponentin semanttiset ominaisuudet määrittelevät yleistä käsitteistöä käyttäen, mitä komponentti tekee. Semantiikan kuvaukseen käytetään pääasiassa ontologisia käsitteitä ja semanttisissa vertailuissa käytetään avuksi logiikkaa.
Komponentin ulkoinen käyttäytymiskuvaus ilmaisee sen käyttäytymismallin, jota kyseinen komponentti tukee. Käyttäytymiskuvaus on sekä ohje että rajoitus, joka toisaalta antaa mallin oikeelliselle vuorovaikutukselle ja toisaalta toimii komponenttien välisen korvautuvuuden tarkistusehtona. Komponentin ulkoinen käyttäytyminen, niin kutsuttu rajapintaprotokolla, kuvataan käyttäen prosessialgebraa. Tässä opinnäytetyössä on prosessialgebraksi valittu π-kalkyyli.
Kun komponenttien ominaisuudet on mallinnettu formaalisti, voidaan komponenttien välinen yhteensopivuus ja korvautuvuus tarkistaa ohjelmallisesti. Tällaista ohjelmistoa voidaan hyödyntää esimerkiksi ohjelmiston suunnitteluprosessissa.
