Original title: Automaty ve Verifikaci a Testování Software
Translated title: Automata in Software Verification and Testing
Authors: Hruška, Martin ; Rezine, Ahmed (referee) ; Kofroň, Jan (referee) ; Vojnar, Tomáš (advisor)
Document type: Doctoral theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Tato práce se zabývá aplikacemi teorie automatů v zajištění kvality software. V první části se zabývá aplikací automatů v tzv. analýze tvaru, kterou lze využít pro formální verifikaci programů pracujících s dynamickými datovými strukturami. Konkrétně představuje rozšíření analýzy tvaru založené na lesních automatech o zpětný běh analýzy přes řádky programu, které se objeví v potenciálním protipříkladu a zjemnění abstrakce založené protipříkladech. Dále je v práci představena nová doména pro analýzu tvaru a to automaty nad grafy s omezenou stromovou šířkou. Ty jsou obecnější než lesní automaty, ale zároveň výpočetní složitost algoritmů s nimi pracujících je použitelná. V druhé části se zabýváme automatizovaným testováním výrobních informačních systémů v prostředí digitálního dvojčete. Představujeme metodu, která dokáže orchestrovat digitální dvojče tak, aby reprodukovalo reálné prostředí, v němž bývají zmíněné systémy nasazeny. To poskytuje bezpečné prostředí testování výrobních informačních systémů. Navíc jsme metodu rozšířili o možnost tvorby nových testovacích scénářů nad rámec pouhé reprodukce již pozorovaného chování reálného prostředí, a tak zvýšili kvalitu testovacího procesu. This thesis focuses on applications of automata theory to software quality. In the first part, we focus on shape analysis which can be used for formal verification of programs manipulating dynamic data structures. Particularly, we develop an approach of backward program execution along possible counterexamples tracesvand counterexample-guided refinement for shape analysis based on forest automata. We also introduce a new approach based on automata over graphs with a bounded tree width which is more general than forest automata but still has feasible computation properties. In the second part, we introduce a method for automated testing of manufacturing execution systems (MES) in digital twin. We are able to orchestrate a digital twin to reproduce behaviour of a real-world setting in which MES is deployed and so provide a safe environment for testing. Moreover, we can generate new test cases by applying automata and abstraction over them in this context.
Keywords: analýza tvaru; formální verifikace; konečné automaty; statická analýza; testování; finite automata; formal verification; shape analysis; static analysis; testing

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/249420

Permalink: http://www.nusl.cz/ntk/nusl-623616


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Doctoral theses