Automatized Data Abstraction

Abstract

Model checking patří mezi nejrozšířenější metody verifikace softwarových systémů. Během verifikace pomocí této metody se prochází celý stavový prostor daného systému. Stavový prostor softwarových systémů je ale obrovský a není tedy možné ho celý projít v rozumném čase. Tento problem se nazývá "state explosion problem" a jednou z metod, jak ho řešit, je použití abstrakce, kdy se konkrétní data verifikovaného systému namapují na abstraktní data. Výsledný abstraktní systém pokrývá chování původního systému nezbytné pro verifikaci, ale má výrazně menší stavový prostor, což umožňuje jeho verifikaci v rozumném čase. Tato práce se zabývá automatickou abstrakcí dat. Shrnuje známé metody automatické abstrakce, tyto metody porovnává a na základě získaných vědomostí navrhuje novou metodu automatické abstrakce pro objektově orientované systémy.

Model checking belongs to one of the most favourite techniques for verification of software systems. During the verification process of model checking, the whole state space of the given system is traversed. However, the state space of software systems can be huge and thus it is not possible to traverse it in reasonable amount of time. This problem is called "state explosion problem" and it can be solved using a method of abstraction that creates an abstract program from the concrete one by mapping the concrete data to abstract data. The abstract program covers all the behavior of the concrete program that is necessary for verification, but has significantly smaller state space which allows its verification in reasonable amount of time. This work is concerned in automatized data abstraction. Three known methods for automatized data abstraction are described and compared to each other. Based on these methods a new method for automatized data abstraction of object oriented programs is designed.