Extending Verification of Industrial TNSDL Programs with Formal Methods by Using EMMA
No Thumbnail Available
URL
Journal Title
Journal ISSN
Volume Title
Helsinki University of Technology |
Diplomityö
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Authors
Date
1998
Department
Major/Subject
Digitaalitekniikka
Mcode
Tik-79
Degree programme
Language
en
Pages
iv + 66
Series
Abstract
Tässä työssä esitellään formaaleihin menetelmiin perustuvan rinnakkaisohjelmistojen analysaattorin EMMAn evaluointi teollisessa ympäristössä. Evaluoinnin tarkoituksena oli arvioida analysaattorin käytön tarjoamia mahdollisuuksia Nokia Telecommunications:n telejärjestelmien ohjelmistokehitysprosessille erityisesti TNSDL-ohjelmointikielen käyttöön liittyviltä osilta. Saavutettavuusanalyysiin perustuva analysaattori helpottaa merkittävästi rinnakkaiskäyttäytymiseen liittyvien ongelmien kuten lukkiumien löytämistä sekä muiden järjestelmän tiloihin liittyvien osoitusten tekemistä. Analysaattori tarjoaa lupaavan vaihtoehdon testikattavuuden kasvattamiseen kustannustehokkaasti, sillä laajalti käytössä olevalla testiajureihin perustuvalla lähestymistavalla on käytännössä mahdotonta saavuttaa 100 %:n kattavuutta. EMMA-analysaattorin kykyä löytää virheitä on osoitettu esimerkkien avulla. Analysaattoria voidaan käyttää TNSDL-ohjelmointikielellä toteutettujen tai määriteltyjen ohjelmistonosien analysointiin tietyin rajoituksin. Nämä rajoitukset on kuvattu ja niiden mahdollisia kiertotapoja on esitetty. Analysaattorin käyttö edellyttää muutoksia analysoitavaan ohjelmistoon. Muutostarpeet on yksilöity sekä niiden toteuttaminen ja vaikutukset analyysituloksiin on määritelty yksikäsitteisesti.Description
Supervisor
Ojala, LeoThesis advisor
Husberg, NisseKeywords
formal methods, TNSDL, Predicate/Transition nets, formaalit menetelmät, reachability analysis, ohjelmistosuunnittelu, software development, Predikaatti/Transitio -verkot, TNSDL, saavutettavuusanalyysi, verification, verifiointi