search query: @keyword verifiointi / total: 19
reference: 13 / 19
Author: | Manner, Tapio |
Title: | Extending Verification of Industrial TNSDL Programs with Formal Methods by Using EMMA |
Teollisten TNSDL ohjelmien verifioinnin laajentaminen formaaleilla menetelmillä käyttäen EMMA järjestelmää | |
Publication type: | Master's thesis |
Publication year: | 1998 |
Pages: | iv + 66 Language: eng |
Department/School: | Tietotekniikan osasto |
Main subject: | Digitaalitekniikka (Tik-79) |
Supervisor: | Ojala, Leo |
Instructor: | Husberg, Nisse |
OEVS: | Electronic archive copy is available via Aalto Thesis Database.
Instructions Reading digital theses in the closed network of the Aalto University Harald Herlin Learning CentreIn the closed network of Learning Centre you can read digital and digitized theses not available in the open network. The Learning Centre contact details and opening hours: https://learningcentre.aalto.fi/en/harald-herlin-learning-centre/ You can read theses on the Learning Centre customer computers, which are available on all floors.
Logging on to the customer computers
Opening a thesis
Reading the thesis
Printing the thesis
|
Location: | P1 Ark T80 | Archive |
Keywords: | formal methods Predicate/Transition nets reachability analysis software development TNSDL verification TNSDL formaalit menetelmät ohjelmistosuunnittelu Predikaatti/Transitio -verkot saavutettavuusanalyysi verifiointi |
Abstract (fin): | 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. |
ED: | 1999-02-02 |
INSSI record number: 13858
+ add basket
INSSI