An algorithm and case study for the object oriented abstraction

Jakub Ratajczak

Abstract


Model checking of software systems becomes more effective each day. However it still can not handle huge state spaces of real software. Particularly, concurrent systems are hard to verify. Abstraction techniques are one of the solutions aimed at managing the complexity problem. This paper describes the object oriented abstraction algorithm. It allows semi-automatic abstraction of real (i.e. Java) programs. A novelty method for constructing class abstractions is shown. It uses additional program annotations expressed in a formal manner. Proposed techniques are shown in a context of algorithms used in the Bandera toolset. A short case study of this approach is also shown.

Full Text:

PDF


DOI: http://dx.doi.org/10.17951/ai.2004.2.1.115-124
Date of publication: 2015-01-04 00:00:00
Date of submission: 2016-04-27 10:11:09


Statistics


Total abstract view - 392
Downloads (from 2020-06-17) - PDF - 0

Indicators



Refbacks

  • There are currently no refbacks.


Copyright (c) 2015 Annales UMCS Sectio AI Informatica

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.