Original title: String constraint solving pro automatickém generování testů pro simulinkové modely
Translated title: String Constraint Solving in Automated Test Generation for Simulink Models
Authors: Ráček, Jakub ; Smrčka, Aleš (referee) ; Holík, Lukáš (advisor)
Document type: Bachelor's theses
Year: 2025
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Verifikace softwaru v bezpečnostně kritických systémech, jako jsou systémy řízení letu, vyžaduje rigorózní procesy, včetně zajištění sledovatelnosti od požadavků k testovacím vektorům. Navrhujeme způsob, jak plně využít SMT řešič Z3-Noodler pro automatické generování testovacích vektorů na základě požadavků pro Simulinkové modely, což umožňuje efektivní zpracování datového typu řetězec. Naše metodologie zahrnuje zjednodušenou formalizaci sémantiky modelů Simulinku, která je použita k definování chování nových bloků pro manipulaci s řetězci vytvořených pro Simulinkovou knihovnu BLADE. Tato formalizace také řídí jejich překlad do SMT omezení. Prototyp demonstrující tento přístup byl implementován v rámci nástroje pro generování testů SAMWISE, vyvinutého ve spolupráci mezi VUT a společností Honeywell. Prototyp překládá modely Simulinku s těmito řetězcovými bloky do interní reprezentace PySMT, což umožňuje SMT řešičům generovat testovací vektory na základě uživatelem definovaných požadavků. Experimentální vyhodnocení na srovnávacích modelech prokazuje funkčnost přístupu a úspěšně generuje validní testovací vektory, které byly ověřeny pomocí průmyslového testovacího prostředí. Software verification of safety-critical systems, such as flight controls, demands rigorous processes, such as ensuring traceability from requirements to test vectors. We propose a way to harness the SMT solver Z3-Noodler for the automatic generation of test vectors based on requirements for Simulink models, which allows for effective handling of the string data type. Our methodology involves a simplified formalization of Simulink model semantics, which is used to define the behavior of new string-manipulating blocks created for the BLADE Simulink library. This formalization guides their translation into SMT constraints. A prototype demonstrating this approach has been implemented within the SAMWISE test generation tool and developed in collaboration between BUT and Honeywell. The prototype translates Simulink models with these string blocks into an internal PySMT representation, enabling SMT solvers to generate test vectors based on user-defined requirements. Experimental evaluation on benchmark models demonstrates the functionality of the approach, successfully generating valid test vectors that were verified using an industrial test harness.
Keywords: Automatické generování testů; Simulink; SMT solving; verifikace sofwaru; řetězcová omezení; Automated test generation; Simulink; SMT solving; software verification; string constraints

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/253724

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


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