An algorithm and case study for the object oriented abstraction
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:
PDFDOI: 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
This work is licensed under a Creative Commons Attribution 4.0 International License.