search query: @author Juslin, Veli-Pekka / total: 1
reference: 1 / 1
« previous | next »
Author: | Juslin, Veli-Pekka |
Title: | A practical model checking approach using SATABS |
Käytännön lähestymistapa mallintarkastukseen SATABS -verifiointityökalua käyttäen | |
Publication type: | Master's thesis |
Publication year: | 2010 |
Pages: | iv + 66 Language: eng |
Department/School: | Informaatio- ja luonnontieteiden tiedekunta |
Main subject: | Tietojenkäsittelyteoria (T-119) |
Supervisor: | Niemelä, Ilkka |
Instructor: | |
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 Aalto | Archive |
Keywords: | verification model checking modular verification verifiointi mallintarkistin modulaarinen verifiointi |
Abstract (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. |
Abstract (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. |
ED: | 2010-05-10 |
INSSI record number: 39582
+ add basket
« previous | next »
INSSI