Generalizing lazy abstraction refinement algorithms with partial orders. Cziborová, D. 2021. Bachelor's Thesis, Budapest University of Technology and Economics![Generalizing lazy abstraction refinement algorithms with partial orders [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Pdf abstract bibtex 3 downloads Safety verification of software systems is a key challenge in the development of critical real-time embedded systems. In automated software model checking, a formal description of the system is checked against the desired safety properties by an automated tool. However, model checking systems of even a moderate size can be difficult. For systems with a finite number of possible behavior, the number of states that has to be traversed during model checking often grows exponentially in the size of the system. Moreover, taking timing into account requires reasoning with an uncountably infinite set of states. To provide a compact representation of the state space, various abstraction-based techniques were introduced in the literature. Among these techniques, lazy abstraction and its variants provide an efficient solution for the analysis of timed models with data. The various characteristics of the programs being analyzed necessitate different kinds of lazy abstractions. There is no single best algorithm; therefore, there is a need for a configurable lazy abstraction framework as a generalization of the available approaches. Our work aims to provide a configurable lazy abstraction framework by adapting the theory of partial orders and Galois connections to lazy abstractions. In particular, we (i) define a general (theoretical) framework of lazy abstraction refinement; (ii) integrate the existing lazy abstraction techniques into the framework; (iii) provide new combinations and configurations of the lazy abstraction techniques; and (iv) implement a lazy abstraction based model checker in the open source Theta tool. We evaluate the applicability of the algorithms on benchmark models.
@misc{cziborovadBsc2021,
author = {Cziborov{\'a}, D{\'o}ra},
title = {Generalizing lazy abstraction refinement algorithms with partial orders},
note = {Bachelor's Thesis, Budapest University of Technology and Economics},
year = {2021},
school = {Budapest University of Technology and Economics},
type = {Thesis},
url_pdf = {cziborovadBsc2021.pdf},
abstract = {Safety verification of software systems is a key challenge in the development of critical real-time embedded systems. In automated software model checking, a formal description of the system is checked against the desired safety properties by an automated tool. However, model checking systems of even a moderate size can be difficult. For systems with a finite number of possible behavior, the number of states that has to be traversed during model checking often grows exponentially in the size of the system. Moreover, taking timing into account requires reasoning with an uncountably infinite set of states. To provide a compact representation of the state space, various abstraction-based techniques were introduced in the literature. Among these techniques, lazy abstraction and its variants provide an efficient solution for the analysis of timed models with data. The various characteristics of the programs being analyzed necessitate different kinds of lazy abstractions. There is no single best algorithm; therefore, there is a need for a configurable lazy abstraction framework as a generalization of the available approaches. Our work aims to provide a configurable lazy abstraction framework by adapting the theory of partial orders and Galois connections to lazy abstractions. In particular, we (i) define a general (theoretical) framework of lazy abstraction refinement; (ii) integrate the existing lazy abstraction techniques into the framework; (iii) provide new combinations and configurations of the lazy abstraction techniques; and (iv) implement a lazy abstraction based model checker in the open source Theta tool. We evaluate the applicability of the algorithms on benchmark models.},
}
Downloads: 3
{"_id":"vcWqp9SmG4krXHWkn","bibbaseid":"cziborov-generalizinglazyabstractionrefinementalgorithmswithpartialorders-2021","author_short":["Cziborová, D."],"bibdata":{"bibtype":"misc","type":"Thesis","author":[{"propositions":[],"lastnames":["Cziborová"],"firstnames":["Dóra"],"suffixes":[]}],"title":"Generalizing lazy abstraction refinement algorithms with partial orders","note":"Bachelor's Thesis, Budapest University of Technology and Economics","year":"2021","school":"Budapest University of Technology and Economics","url_pdf":"cziborovadBsc2021.pdf","abstract":"Safety verification of software systems is a key challenge in the development of critical real-time embedded systems. In automated software model checking, a formal description of the system is checked against the desired safety properties by an automated tool. However, model checking systems of even a moderate size can be difficult. For systems with a finite number of possible behavior, the number of states that has to be traversed during model checking often grows exponentially in the size of the system. Moreover, taking timing into account requires reasoning with an uncountably infinite set of states. To provide a compact representation of the state space, various abstraction-based techniques were introduced in the literature. Among these techniques, lazy abstraction and its variants provide an efficient solution for the analysis of timed models with data. The various characteristics of the programs being analyzed necessitate different kinds of lazy abstractions. There is no single best algorithm; therefore, there is a need for a configurable lazy abstraction framework as a generalization of the available approaches. Our work aims to provide a configurable lazy abstraction framework by adapting the theory of partial orders and Galois connections to lazy abstractions. In particular, we (i) define a general (theoretical) framework of lazy abstraction refinement; (ii) integrate the existing lazy abstraction techniques into the framework; (iii) provide new combinations and configurations of the lazy abstraction techniques; and (iv) implement a lazy abstraction based model checker in the open source Theta tool. We evaluate the applicability of the algorithms on benchmark models.","bibtex":"@misc{cziborovadBsc2021,\n author = {Cziborov{\\'a}, D{\\'o}ra},\n title = {Generalizing lazy abstraction refinement algorithms with partial orders},\n note = {Bachelor's Thesis, Budapest University of Technology and Economics},\n year = {2021},\n school = {Budapest University of Technology and Economics},\n type = {Thesis},\n url_pdf = {cziborovadBsc2021.pdf},\n abstract = {Safety verification of software systems is a key challenge in the development of critical real-time embedded systems. In automated software model checking, a formal description of the system is checked against the desired safety properties by an automated tool. However, model checking systems of even a moderate size can be difficult. For systems with a finite number of possible behavior, the number of states that has to be traversed during model checking often grows exponentially in the size of the system. Moreover, taking timing into account requires reasoning with an uncountably infinite set of states. To provide a compact representation of the state space, various abstraction-based techniques were introduced in the literature. Among these techniques, lazy abstraction and its variants provide an efficient solution for the analysis of timed models with data. The various characteristics of the programs being analyzed necessitate different kinds of lazy abstractions. There is no single best algorithm; therefore, there is a need for a configurable lazy abstraction framework as a generalization of the available approaches. Our work aims to provide a configurable lazy abstraction framework by adapting the theory of partial orders and Galois connections to lazy abstractions. In particular, we (i) define a general (theoretical) framework of lazy abstraction refinement; (ii) integrate the existing lazy abstraction techniques into the framework; (iii) provide new combinations and configurations of the lazy abstraction techniques; and (iv) implement a lazy abstraction based model checker in the open source Theta tool. We evaluate the applicability of the algorithms on benchmark models.},\n}\n\n","author_short":["Cziborová, D."],"key":"cziborovadBsc2021","id":"cziborovadBsc2021","bibbaseid":"cziborov-generalizinglazyabstractionrefinementalgorithmswithpartialorders-2021","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/cziborovadBsc2021.pdf"},"metadata":{"authorlinks":{}},"downloads":3},"bibtype":"misc","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","dataSources":["7MDizr2BZojXoNdPN"],"keywords":[],"search_terms":["generalizing","lazy","abstraction","refinement","algorithms","partial","orders","cziborová"],"title":"Generalizing lazy abstraction refinement algorithms with partial orders","year":2021,"downloads":3}