haku: @keyword model checking / yhteensä: 20
viite: 4 / 20
| Tekijä: | Juslin, Veli-Pekka |
| Työn nimi: | A practical model checking approach using SATABS |
| Käytännön lähestymistapa mallintarkastukseen SATABS -verifiointityökalua käyttäen | |
| Julkaisutyyppi: | Diplomityö |
| Julkaisuvuosi: | 2010 |
| Sivut: | iv + 66 Kieli: eng |
| Koulu/Laitos/Osasto: | Informaatio- ja luonnontieteiden tiedekunta |
| Oppiaine: | Tietojenkäsittelyteoria (T-119) |
| Valvoja: | Niemelä, Ilkka |
| Ohjaaja: | |
| OEVS: | Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossaOppimiskeskuksen suljetussa verkossa voi lukea sellaisia digitaalisia ja digitoituja opinnäytteitä, joille ei ole saatu julkaisulupaa avoimessa verkossa. Oppimiskeskuksen yhteystiedot ja aukioloajat: https://learningcentre.aalto.fi/fi/harald-herlin-oppimiskeskus/ Opinnäytteitä voi lukea Oppimiskeskuksen asiakaskoneilla, joita löytyy kaikista kerroksista.
Kirjautuminen asiakaskoneille
Opinnäytteen avaaminen
Opinnäytteen lukeminen
Opinnäytteen tulostus
|
| Sijainti: | P1 Ark Aalto | Arkisto |
| Avainsanat: | verification model checking modular verification verifiointi mallintarkistin modulaarinen verifiointi |
| Tiivistelmä (fin): | Tämän työn tavoitteena on tutkia mallintarkastukseen pohjautuvien formaalien verifiointimenetelmien soveltuvuutta ketteriin ja epäformaaleihin ohjelmistonkehitysprosesseihin, joille ominaista on kehitettävän ohjelmiston formaalin määrittelyn puuttuminen. Erityisenä tavoitteena on kyetä täydentämään testausta ja heuristisia virheenetsintämenetelmiä formaalilla mallintarkastukseen perustuvalla koodin analysoinnilla ilman merkittäviä muutoksia olemassa oleviin ohjelmistokehitysprosesseihin. SATABS-verifiointityökalu ANSI-C ja C++ -lähdekoodille on valittu tähän työhön pääasiassa, koska verifiointi voidaan suorittaa suoraan lähdekoodista ilman erillistä formaalia määrittelyä. Analysoitavina esimerkkeinä käytetään avoimena lähdekoodina julkaistun GNU Coreutils -työkaluohjelmapaketin raportoituja ohjelmavirheitä. Työssä tutkitaan ovatko ohjelmavirheet löydettävissä SATABS-veriflointityökalua käyttäen. Lähdekoodia pyritään vuorotellen verifioimaan ja modifioimaan verifiointityökalun edellyttämällä tavalla, kunnes tämä tuottaa odotettuja tuloksia eli raportoi ennalta tunnetut ohjelmavirheet. Tulokset osoittavat, että koko lähdekoodin verifiointi mallintarkastukseen pohjautuvin menetelmin yhtenä kokonaisuutena ei ole käytännössä mahdollista edes kohtuullisen suppeiden ja yksinkertaisten ohjelmien osalta. Kuitenkin, jos luovutaan verifioinnin oikeellisuuden ja täydellisyyden vaatimuksista, voidaan käytännössä hyödyllisiä tuloksia saada pilkkomalla verifiointiongelma pienempiin osaongelmiin. Tulokset osoittavat myös, että pilkkomisen jälkeen verifioinnin edellyttämät koodimuutokset ovat verrattain vähäisiä, ja voidaan realistisesti olettaa ne voitavan huomioida jo ohjelmankehitysvaiheessa. Osittaisena ratkaisuna verifioinnin kustannusongelmiin esitetään epätäydellinen virheenetsintäalgoritmi perustuen ohjelmakoodin abstrahointiin ja vaiheittaiseen tarkentamiseen funktiokutsujen tarkkuudella. Algoritmin käyttökelpoisuus demonstroidaan esimerkillä. Työssä myös esitetään ohjelmien siivutusta (program slicing) osana virheenetsintäalgoritmia. |
| Tiivistelmä (eng): | The goal of this work is to study the applicability of model checking methods to agile and informal non-specialized software development processes characterized by lack of a formal specification. The emphasis is in complementing testing and heuristic bug-finding methods with formal program analysis based on model checking without significant modifications to existing software processes. Without a formal specification, all verifiable design intent including user-defined arbitrary assertions are conveyed in the source code. SATABS, a model checking -based software verification tool for ANSI-C and C++- has been selected for this work primarily since it is capable of deriving all checked claims directly from the source code requiring no separately constructed external specification. As a case study, bugs detected in utilities contained in GNU Coreutils open source toolkit are analysed. The feasibility of detecting these bugs with SATABS is evaluated. Iteratively, starting with unmodified source code, verification using SATABS is attempted and the source code is modified according to the results until verification yields expected results as the a priori known bugs are reported. The results indicate that monolithic verification of the entire code base is still infeasible even with relatively small and uncomplicated non-threaded programs. However, if requirements for soundness and completeness are relaxed, useful results can be obtained using divide-and-conquer strategies. Results also indicate that the code modifications required by SATABS are relatively simple when divide-and-conquer strategies are used, and could realistically be incorporated in the program by a software engineer or a programmer with good working knowledge of the tool. As a partial solution to verification affordability problems, an incomplete bug-finding algorithm based on abstraction and piecewise refinement of source code at function call granularity is presented and its practical usefulness demonstrated. Also, using a program slicer such as implemented in FRAMA-C embedded in a bug-finding algorithm is proposed. |
| ED: | 2010-05-10 |
INSSI tietueen numero: 39582
+ lisää koriin
INSSI