search query: @keyword verifiointi / total: 19
reference: 4 / 19
« 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 Centre

In 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

  • Aalto University staff members log on to the customer computer using the Aalto username and password.
  • Other customers log on using a shared username and password.

Opening a thesis

  • On the desktop of the customer computers, you will find an icon titled:

    Aalto Thesis Database

  • Click on the icon to search for and open the thesis you are looking for from Aaltodoc database. You can find the thesis file by clicking the link on the OEV or OEVS field.

Reading the thesis

  • You can either print the thesis or read it on the customer computer screen.
  • You cannot save the thesis file on a flash drive or email it.
  • You cannot copy text or images from the file.
  • You cannot edit the file.

Printing the thesis

  • You can print the thesis for your personal study or research use.
  • Aalto University students and staff members may print black-and-white prints on the PrintingPoint devices when using the computer with personal Aalto username and password. Color printing is possible using the printer u90203-psc3, which is located near the customer service. Color printing is subject to a charge to Aalto University students and staff members.
  • Other customers can use the printer u90203-psc3. All printing is subject to a charge to non-University members.
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