@misc{mondokmBsc2020,
    author = {Mondok, Mil\'an},
    title = {Formal verification of engineering models via extended symbolic transition systems},
    note = {Bachelor's Thesis, Budapest University of Technology and Economics},
    year = {2020},
    type = {Thesis},
    url_pdf = {mondokmBsc2020.pdf},
    url_link = {https://diplomaterv.vik.bme.hu/hu/Theses/Mernoki-modellek-formalis-verifikacioja},
    abstract = {In a model-driven development workflow, formal verification can give early feedback on the correctness of the system under development. However, formal methods face various challenges in practice. First, engineering models are typically developed in higher-level modeling languages, whereas formal methods usually operate on low-level mathematical formalisms. Second, verification algorithms are resource-intensive, especially on complex engineering models. Theta is a generic and configurable verification framework that aims to tackle these challenges by providing different low-level formalisms and efficient, abstraction-based algorithms. However, existing formalisms are either too low-level or domain-specific for model-driven development in general. In this work I propose a novel intermediate representation, the eXtended Symbolic Transition System (XSTS) formalism. The XSTS formalism offers higher-level constructs and a textual domain-specific language for easier translation from engineering models. In the meantime, it also has clear and well-defined semantics under different abstract domains, and adapts a standard interpreter interface towards existing verification algorithms. Furthermore, I developed XSTS-specific extensions and strategies that can improve the performance. My work was integrated into the Gamma Statechart Composition Framework, allowing me to perform an experimental evaluation on use cases provided by industrial partners. I evaluated the strengths and weaknesses of the different algorithm configurations and the results confirmed that the XSTS formalism is both effective and efficient.},
}

{"_id":"eZ9K4HWF49B6nYbbk","bibbaseid":"mondok-formalverificationofengineeringmodelsviaextendedsymbolictransitionsystems-2020","authorIDs":[],"author_short":["Mondok, M."],"bibdata":{"bibtype":"misc","type":"Thesis","author":[{"propositions":[],"lastnames":["Mondok"],"firstnames":["Milán"],"suffixes":[]}],"title":"Formal verification of engineering models via extended symbolic transition systems","note":"Bachelor's Thesis, Budapest University of Technology and Economics","year":"2020","url_pdf":"mondokmBsc2020.pdf","url_link":"https://diplomaterv.vik.bme.hu/hu/Theses/Mernoki-modellek-formalis-verifikacioja","abstract":"In a model-driven development workflow, formal verification can give early feedback on the correctness of the system under development. However, formal methods face various challenges in practice. First, engineering models are typically developed in higher-level modeling languages, whereas formal methods usually operate on low-level mathematical formalisms. Second, verification algorithms are resource-intensive, especially on complex engineering models. Theta is a generic and configurable verification framework that aims to tackle these challenges by providing different low-level formalisms and efficient, abstraction-based algorithms. However, existing formalisms are either too low-level or domain-specific for model-driven development in general. In this work I propose a novel intermediate representation, the eXtended Symbolic Transition System (XSTS) formalism. The XSTS formalism offers higher-level constructs and a textual domain-specific language for easier translation from engineering models. In the meantime, it also has clear and well-defined semantics under different abstract domains, and adapts a standard interpreter interface towards existing verification algorithms. Furthermore, I developed XSTS-specific extensions and strategies that can improve the performance. My work was integrated into the Gamma Statechart Composition Framework, allowing me to perform an experimental evaluation on use cases provided by industrial partners. I evaluated the strengths and weaknesses of the different algorithm configurations and the results confirmed that the XSTS formalism is both effective and efficient.","bibtex":"@misc{mondokmBsc2020,\n author = {Mondok, Mil\\'an},\n title = {Formal verification of engineering models via extended symbolic transition systems},\n note = {Bachelor's Thesis, Budapest University of Technology and Economics},\n year = {2020},\n type = {Thesis},\n url_pdf = {mondokmBsc2020.pdf},\n url_link = {https://diplomaterv.vik.bme.hu/hu/Theses/Mernoki-modellek-formalis-verifikacioja},\n abstract = {In a model-driven development workflow, formal verification can give early feedback on the correctness of the system under development. However, formal methods face various challenges in practice. First, engineering models are typically developed in higher-level modeling languages, whereas formal methods usually operate on low-level mathematical formalisms. Second, verification algorithms are resource-intensive, especially on complex engineering models. Theta is a generic and configurable verification framework that aims to tackle these challenges by providing different low-level formalisms and efficient, abstraction-based algorithms. However, existing formalisms are either too low-level or domain-specific for model-driven development in general. In this work I propose a novel intermediate representation, the eXtended Symbolic Transition System (XSTS) formalism. The XSTS formalism offers higher-level constructs and a textual domain-specific language for easier translation from engineering models. In the meantime, it also has clear and well-defined semantics under different abstract domains, and adapts a standard interpreter interface towards existing verification algorithms. Furthermore, I developed XSTS-specific extensions and strategies that can improve the performance. My work was integrated into the Gamma Statechart Composition Framework, allowing me to perform an experimental evaluation on use cases provided by industrial partners. I evaluated the strengths and weaknesses of the different algorithm configurations and the results confirmed that the XSTS formalism is both effective and efficient.},\n}\n\n","author_short":["Mondok, M."],"key":"mondokmBsc2020","id":"mondokmBsc2020","bibbaseid":"mondok-formalverificationofengineeringmodelsviaextendedsymbolictransitionsystems-2020","role":"author","urls":{" pdf":"https://ftsrg.mit.bme.hu/theta/publications/mondokmBsc2020.pdf"," link":"https://diplomaterv.vik.bme.hu/hu/Theses/Mernoki-modellek-formalis-verifikacioja"},"metadata":{"authorlinks":{}},"downloads":27},"bibtype":"misc","biburl":"https://ftsrg.mit.bme.hu/theta/publications/publications.bib","creationDate":"2021-01-11T18:14:06.593Z","downloads":27,"keywords":[],"search_terms":["formal","verification","engineering","models","via","extended","symbolic","transition","systems","mondok"],"title":"Formal verification of engineering models via extended symbolic transition systems","year":2020,"dataSources":["7MDizr2BZojXoNdPN"]}