Compendium of Documents About the Design and Testing System YERITH_QVGE (YRI_QVGE)

YERITH_QVGE-definitions---cheat--sheet 2 YERITH_QVGE-user-guide 23 YERITHr&d |User’s Cheat Sheet for YRI_SD_RUNTIME_VERIF : A C++ Functional Library for Specifying ”SDMM” (State Diagram Mealy Machine) User’s Cheat Sheet for YRI_SD_RUNTIME_VERIF : AC++ Functional Library for Specifying ”SDMM” (State Diagram Mealy Machine) AUTHOR: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Contact: [email protected] Contents Contents 1 List of Figures 2 List of Tables 3 1 Motivation for SDMM’s Runtime Monitoring Verification Library ”YRI_SD_RUNTIME_VERIF”6 1.1 A Sample Use–Case Scenario of ”SDMM”..................................................... 6 1.2 WHY DO I NEED FORMAL METHODS ....................................................... 6 1.2.1 ”C++ library YRI_SD_RUNTIME_VERIF”: Expressing of sequencing of actions in time (temporal usage rules for system safety) ....................................................................... 6 1.3 Comparison with Unit Testing ............................................................ 6 1.3.1 Unit Testing ................................................................... 6 1.3.2 Automated Unit Testing ........................................................... 6 1.3.3 Runtime Monitoring Verification ...................................................... 6 1.4 State Diagram Mealy Machine : Usages & Advantages ............................................. 7 1.4.1 Usages ...................................................................... 7 1.4.2 Advantages ................................................................... 7 1.4.3 Cases of Practical Usages of ”SDMM” .................................................. 7 1.5 State Diagram Mealy Machine : Brief Summary Explanation ......................................... 7 1.6 Related State Diagram Formalisms ......................................................... 8 1.6.1 David Harel Statechart : A Visual Formalism for State Diagram .................................. 8 1.6.2 Timed Discrete Input / Output Hybrid System (TDIOHS) ....................................... 8 1.6.3 TDIOHS in Action within ”Borland Together 6”with RT–Tester of ’verified.de’........................ 8 1.6.4 TDIOHS in Action by ”Automatic Test Cases / Data Generation” ................................. 9 2 Mathematical Formal Definition of SDMM 9 2.1 Definition 1: A state diagram (for mealy machine). ............................................... 9 2.2 Definition 2: A pre-condition. ............................................................ 9 2.3 Definition 3: A post-condition. ............................................................ 9 2.4 Definition 4: A trace. .................................................................. 10 2.5 SUT Event Processing Method YRI_trigger_an_edge_event ................................... 10 2.5.1 Proposition 1: NO FALSE WARNINGS. .................................................. 10 2.5.2 Explanation on HOW to avoid code that creates False Warnings (False Positives) ...................... 10 2.6 Guarded Condition Expression Specification in YRI_SD_RUNTIME_VERIF ................................... 10 2.7 SDMM for modeling parallel-concurrent software system .......................................... 10 2.8 SDMM in Action within YRI_QVGE by ’Yerith R&D’ ............................................... 10 2.9 SDMM in Action by automatic ”Runtime Monitors Automatic Generation” ................................ 10 3 HOW TO Setup C++ Library ”YRI_SD_RUNTIME_VERIF” for Usage in A C++ PROGRAM SOURCE CODE 10 3.1 Development Toolchain ................................................................ 10 4 METHODS of C++ Library ”YRI_SD_RUNTIME_VERIF”11 4.1 Generated Method YOU need to code ....................................................... 11 5 A Hardware Dedicated Device : YRI–QVGE–PC–Tablet 13 6 Detailed Scientific and Engineering Presentation Document on ’zenodo.org’ 14 7 Conclusion 14 Index 14 Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "1 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d List of Figures 1 A motivating example, as previous bug found in YERITH–ERP–9.0.Q0 :=NOT_IN_BEFORE(YRI_ASSET, department.department_name) ; Q1 := IN_AFTER(YRI_ASSET, stocks.department_name). ..................................................... 4 2 YERITH–ERP–9.0 administration section displaying departments (¬Q0). ................................. 4 3 YERITH–ERP–9.0 stock asset window listing some assets (Q1). ....................................... 4 4A SAMPLE state diagram mealy machine file. KEYWORDS belonging both to ’engineering ("ERROR_STATE_AUTO")’, and ’science (START_STATE)’ can be intermingled in the same SDMM specification file. ...................... 4 5 SAMPLE USE CASE SCENARIO OF "SDMM ". .................................................. 5 6 A SCREENSHOT OF YERITH_QVGE. ........................................................ 5 7 A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL EVENT LOG. ......................................... 5 9 A Sample David HAREL–Statechart model of the temporal property expressed in fig. 4 : —”Whenever department YRI_ASSET was deleted (event ’DELETE.department.YRI_ASSET’); querying stock table shall not find again an inventory stock in any department named YRI_ASSET”—. ................................................ 8 10 A STCT–symbolic test case tree randomly generated by manual drawing for explanation purposes. ............... 8 Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "2 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d List of Tables 1 STATE DIAGRAM MEALY MACHINE SPECIFICATION KEYWORDS IN YERITH_QVGE. ’AUTO’ KEYWORDS SPECIFIES ALSO SQL QUERY FOR GOING OUT AUTOMATICALLY FROM A FAIL (FORBIDDEN) STATE. (“SEE SECTION ??.“) ..... 4 2 Sample important Classes (prefix YRI_CPP_ to class name) & Methods of C++ Library ”YRI_SD_RUNTIME_VERIF”. ........ 11 3 YERITH_QVGE Toolchain ............................................................... 12 Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "3 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Table 1: STATE DIAGRAM MEALY MACHINE SPECIFICATION KEYWORDS IN YERITH_QVGE. ’AUTO’ KEYWORDS SPECIFIES ALSO SQL QUERY FOR GOING OUT AUTOMATICALLY FROM A FAIL (FORBIDDEN) STATE. (“SEE SECTION ??.“) N◦scientific keywords engineering keywords 1. in_set_trace in_sql_event_log 2. not_in_set_trace not_in_sql_event_log 3. recovery_sql_query recovery_sql_query 4. STATE STATE 5. START_STATE BEGIN_STATE 6. FINAL_STATE ("FINAL_STATE_AUTO") END_STATE ("END_STATE_AUTO") / ERROR_STATE ("ERROR_STATE_AUTO") 7. IN_PRE IN_BEFORE 8. IN_POST IN_AFTER 9. IN_POST_NOP N / A 10. NOT_IN_PRE NOT_IN_BEFORE 11. NOT_IN_POST NOT_IN_BEFORE 12. NOT_IN_POST_NOP N / A Figure 1: A motivating example, as previous bug found in YERITH–ERP–9.0. Q0:=NOT_IN_BEFORE(YRI_ASSET, department.department_name) ; Q1 :=IN_AFTER(YRI_ASSET, stocks.department_name). D Q0 start E Q1 [in_sql_event_log(’DELETE.department.YRI_ASSET’, STATE(D))] / ’SELECT.department’ Figure 2: YERITH–ERP–9.0 administration section displaying departments (¬Q0). Figure 3: YERITH–ERP–9.0 stock asset window listing some assets (Q1). Figure 4: A SAMPLE state diagram mealy machine file. KEYWORDS belonging both to ’engineering ("ERROR_STATE_AUTO")’, and ’science (START_STATE)’ can be intermingled in the same SDMM specification file. 1. yr_sd_mealy_automaton_spec yr_missing_department_NO_DELETE 2. { 3. START_STATE(d):NOT_IN_BEFORE(YRI_ASSET,department.department_name) 4. ->[in_sql_event_log(’DELETE.departement.YRI_ASSET’,STATE(d))]/’SELECT.department’-> 5. ERROR_STATE(e):IN_AFTER(YRI_ASSET,stocks.department_name). 6. } Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "4 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Figure 5: SAMPLE USE CASE SCENARIO OF "SDMM ". Internet parallel process management runtime execution and theard resources. implement YRI−DB−RUNTIME−VERIF A PCI−CARD could also (network) communication QT−Dbus RPC Protocol executes SDMM plugins YRI−DB−RUNTIME−VERIF NETWORK Router (including Firewall) YRI_QVGE CASE tool drawing designs Available also in a USB dongle key YRI−Db−Runtime−Verif Java Developer computer running related drawing designs with Intel−PIN) (REQUIRES JVM re−instrumentation Cyber−Security SDMM enables QT−plugin loading at runtime YRI−DB−RUNTIME−VERIF JVM−Java Virtual Machine IBM Websphere APPLICATION Server / Or for e.g.: Quercus Application Server serving DYNAMIC / STATIC Web Apps DBMS Listing 1: Sample real world ”C++” code as opposed to PSEUDO–CODE ”C++” code; as modified by a developer after automatic generation of YRI-DBRUNTIME-VERIF. 1bool YERITH_QVGE_sample_PAPER_extended_version_PROPERY::DO_VERIFY_AND_or_CHECK_ltl_PROPERTY( 2 QString sql_table_ADDED_with_file_AND_line_number, 3 uint sql_record_qty_MODIFIED, 4 YRI_CPP_UTILS::SQL_CONSTANT_IDENTIFIER cur_SQL_command) 5 { 6 QStringList sql_table_ADDED_with_file_AND_line_number_LIST = sql_table_ADDED_with_file_AND_line_number.split(";", Qt::KeepEmptyParts); 7 QString sql_table_name = sql_table_ADDED_with_file_AND_line_number_LIST.at(0); 8 QString CPP_FILE_NAME = sql_table_ADDED_with_file_AND_line_number_LIST.at(1); 9 QString cpp_line_number = sql_table_ADDED_with_file_AND_line_number_LIST.at(2); 10 11 switch(cur_SQL_command) 12 { 13 case YRI_CPP_UTILS::INSERT: 14 break; 15 16 case YRI_CPP_UTILS::SELECT: 17 if (YRI_DB_RUNTIME_VERIF_Utils::isEqualsCaseInsensitive(sql_table_name, "departements_produits")) { 18 return YRI_SQL_SELECT_departements_produits(); 19 } 20 break; 21 22 case YRI_CPP_UTILS::UPDATE: 23 break; 24 25 case YRI_CPP_UTILS::DELETE: 26 break; 27 28 default: 29 break; 30 } 31 32 return false; 33 } Figure 6: A SCREENSHOT OF YERITH_QVGE. Figure 7: A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL EVENT LOG. Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "5 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Table 3: YERITH_QVGE Toolchain PROJECT Required Program / Library 1)YRI_SD_RUNTIME_VERIF_LANG ”Qt-trolltech” (https://doc.qt.io/qt-5) 2)YRI_SD_RUNTIME_VERIF_LANG_COMP 1) 3)YRI_SD_RUNTIME_VERIF_UNIT_TESTS 1) 4)YRI-DB-RUNTIME-VERIF 2) Table 3illustrates for each library project, which others it depends on. Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "12 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d 5 A Hardware Dedicated Device : YRI–QVGE–PC–Tablet A hardware dedicated device running a runtime monitoring verification device called YRI–DB–RUNTIME–VERIF is in creation by myself. Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "13 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d 6 Detailed Scientific and Engineering Presentation Document on ’zenodo.org’ Detailed formal scientific and engineering contributions of design and testing system YERITH_QVGE can be found in JOURNAL ARTICLE "Runtime Verification Of SQL Correctness Properties with YRI-DB-RUNTIME-VERIF" [nN23]. 7 Conclusion The graphical drawing tool YERITH_QVGE (Figure 6) costs only 2, 500 EUROS. WE ONLY SUPPORT DEBIAN–LINUX (https: //www.debian.org). References [AAC+05] Chris Allan, Pavel Avgustinov, Aske Simon Christensen, Bruno Dufour, Christopher Goard, Laurie J. Hendren, Sascha Kuzins, Jennifer Lhoták, Ondrej Lhoták, Oege de Moor, Damien Sereni, Ganesh Sittampalam, Julian Tibble, and Clark Verbrugge. abc the aspectbench compiler for aspectj a workbench for aspect-oriented programming language and compilers research. In Ralph E. Johnson and Richard P. Gabriel, editors, Companion to the 20th Annual ACM SIGPLAN Conference on ObjectOriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, pages 88–89. ACM, 2005. [BFPT06] B. Badban, M. Fränzle, J. Peleska, and T. Teige. Test automation for hybrid systems. In Third International Workshop on Software Quality Assurance (SOQUA 2006), pages 14–21, 2006. [BH12] Eric Bodden and Laurie Hendren. The clara framework for hybrid typestate analysis. International Journal on Software Tools for Technology Transfer (STTT), 14:307–326, 2012. 10.1007/s10009-010-0183-5. [Bod05] Eric Bodden. J-LO - A tool for runtime-checking temporal assertions. Diploma thesis, RWTH Aachen University, November 2005. [BRBY00] Sergey Butkevich, Marco Renedo, Gerald Baumgartner, and Michal Young. Compiler and tool support for debugging object protocols. In SIGSOFT ’00/FSE-8, 2000. [CGK+18] Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. Model checking, 2nd Edition, 2018. [CR07] Feng Chen and Grigore Rosu. Mop: an efficient and generic runtime verification framework. In Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr., editors, Proceedings of the 22nd Conference on Object-Oriented Programming, Systems, Languages and Applications, pages 569– 588. ACM, 2007. [Gau06] M.-C. Gaudel. ???–test automation for hybrid systems–??? In Third International Workshop on Software Quality Assurance (SOQUA 2006), pages 14–21, 2006. [HarXX] David Harel. Statecharts: a visual formalism for complex systems. https://www.wisdom. weizmann.ac.il/~dharel/SCANNED. PAPERS/Statecharts.pdf, XXXX. Accessed last time on Apr 28,2025 at 12:00. [MYE20] Andrew MYERS. Software testing ..., 20.. [nf10] Serges ACHILLES nono fopoussi. Automatisierte testdatengenerierung hybrider diskretkontinuierlicher eingebetteter systeme. https:// www.deutsche-digitale-bibliothek.de/ person/gnd/141875240, 2010. DOCTORATE THESIS IN COMPUTER SCIENCE (Dr.–Ing.), University of Bremen, Bremen, Bremen, Germany. [NN07] Xavier Noumbissi Noundou. Statistical test cases generation for reactive systems. https://www.informatik.uni-bremen. de/agbs/qualifikationsarbeiten/ diplomarbeiten_e.html, 2007. Integrated Bachelor & Master’s Degree Thesis in Computer Science (B.Sc. & M.Sc.), University of Bremen, Bremen, Bremen, Germany. [nN23] Xavier noumbissi Noundou. A Framework for Verifying SQL Correctness Temporal Properties of GUI Software at Runtime. https://zenodo. org/records/10976659, October 2023. [NN25] Xavier Noumbissi Noundou. A C++ functional library for specifying "SDMM" (state diagram mealy machine). https://www.zenodo.org/ records/10474033, 2025. A C++ Functional Library for Specifying "SDMM". [Nou09] Xavier Noundou. Junit 4tutorial. https: //www.zenodo.org/record/8052444, Oct. 2009. Text–tutorial ”Junit 4”, University of Waterloo, Waterloo, Ontario, Canada. [Nou22] Xavier Noundou. YERITH–ERP–PGI–3.0 Doctoral Compendium. https://archive.org/ download/yerith-erp-pgi-compendium_ 202206/JH_NISSI_ERP_PGI_COMPENDIUM. pdf, June 2022. Accessed last time on January 21, 2023 at 23:24. [PlH21] Jan Peleska and Wen ling Huang. Test automation; foundations and applications of model-based testing. https://www.informatik. uni-bremen.de/agbs/jp/papers/ test-automation-huang-peleska.pdf, July 2021. Accessed last time on May 06,2023 at 12:00. [Ra01] Bill Roscoe and al... CSP : Communicating Sequential Processes. UK, 2nd edition, 2001. [Wik22] Wikipedia.org. Mealy machine. https://en. wikipedia.org/wiki/Mealy_machine, December 2022. Accessed last time on Dec 15,2022 at 12:00. [Zel20] Andreas Zeller. Software testing ..., 20.. Index Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "14 / 16". | Version of – June 1, 2025 – JUnit testing framework, 6 A Sample David HAREL–Statechart model of the temporal property expressed in fig. 4,8 A STCT–symbolic test case tree randomly generated by manual drawing for explanation purposes, 8 Automated Unit Testing, 6 Black–box Testing, 6 Unit Testing, 6 White–box Testing, 6 15 YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "16 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "17 / 16". | Version of – June 1, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "18 / 16". | Version of – June 1, 2025 – YERITHr&d |user’s guide for YERITH_QVGE User’s Guide for the Design and Testing System YERITH_QVGE (YRI_QVGE) AUTHOR: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Contact: [email protected] Contents Contents 1 List of Figures 2 List of Tables 3 1 Introduction 6 2 YERITH_QVGE (YRI_QVGE) Short Overview 6 3 YERITH_QVGE (YRI_QVGE) Project Dependency 7 4 Advantages of YERITH_QVGE 7 5 State Diagram Mealy Machine (SDMM) 7 5.1 HOW TO READ A "SDMM" .............................................................. 7 5.2 "SDMM" WITH MORE THAN 2STATES ...................................................... 7 6 YERITH_QVGE (YRI_QVGE) Workflow 7 7 Custom User Project (YRI–DB–RUNTIME–VERIF) 7 8 HOW TO START YRI-DB-RUNTIME-VERIF 8 9 SQL QUERY Recovery execution on demand 8 9.1 Automatic SQL Command Query Generation .................................................. 8 9.1.1 ERROR ACCEPTING STATE for sdmm 1. ................................................ 9 9.1.2 RECOVERY 1. .................................................................. 9 9.1.3 RECOVERY 2 (Practical solution to be implemented in YRI-DB-RUNTIME-VERIF. ...................... 9 9.1.4 Concrete RECOVERY 2 action. ....................................................... 9 10 HOW TO USE a user interface 9 11 YRI_SD_RUNTIME_VERIF SPECIFICATION LANGUAGE 9 12 Formal Scientific and Engineering Project Description 9 13 Conclusion 9 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "1 / 10". | Version of – June 7, 2025 – YERITH_QVGE user’s guide YERITHr&d List of Figures 1 A motivatingexample, asprevious bugfoundin YERITH–ERP–9.0.Q0 :=NOT_IN_BEFORE(YRI_ASSET, department.department_name); Q1 := IN_AFTER(YRI_ASSET, stocks.department_name). ..................................................... 4 2 YERITH–ERP–9.0 administration section displaying departments (¬Q0). ................................. 4 3 YERITH–ERP–9.0 stock asset window listing some assets (Q1). ....................................... 4 4A SAMPLE state diagram mealy machine file. KEYWORDS belonging both to ’engineering ("ERROR_STATE_AUTO")’, and ’science (START_STATE)’ can be intermingled in the same SDMM specification file. ...................... 4 5 SAMPLE USE CASE SCENARIO OF "SDMM ". .................................................. 5 6 A SCREENSHOT OF YERITH_QVGE. ........................................................ 5 7 A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL EVENT LOG. ....................................... 5 8 SOFTWARE ARCHITECTURE OF YRI-DB-RUNTIME-VERIF. ........................................ 6 9 YERITH_QVGE software library dependencies. ................................................. 6 10 Workflow explanation. ................................................................. 7 11 SAMPLE sql recovery state diagram model in YERITH_QVGE ........................................ 8 12 YERITH_QVGE user interface screenshot. .................................................... 9 13 Grammar in Backus–Naur Form (BNF) of YRI_SD_RUNTIME_VERIF_LANG Mealy Machine STATE DIAGRAM Specification Language. ......................................................................... 10 Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "2 / 10". | Version of – June 7, 2025 – YERITH_QVGE user’s guide YERITHr&d 3 YERITH_QVGE (YRI_QVGE) Project Dependency Table 2: YERITH_QVGE Design and Testing System Dependencies PROJECT Required Program / Library 1)YRI_SD_RUNTIME_VERIF_LANG 2)YRI_SD_RUNTIME_VERIF_LANG_COMP 1) 3)YRI_SD_RUNTIME_VERIF_UNIT_TESTS 1) 4)YRI-DB-RUNTIME-VERIF 2) Table 2illustrates for each library project, which others it depends on. 4 Advantages of YERITH_QVGE A sample state diagram mealy machine is shown in Figure 4. WITH manual drawing of SQL CORRECTNESS PROPERTY MODEL, you are freed from manually writing "state diagram mealy machine text files" that could be tedious and lengthy. Also, editing state diagram mealy machine files manually could be more error-prone than letting a compiler (YRI_SD_RUNTIME_VERIF_LANG) do it for you. 5 State Diagram Mealy Machine (SDMM) TABLE 1depicts scientific keywords and their engineering counterpart that can be used in describing NOT DESIRABLE 3 SQL 4call sequence state diagram mealy machine in YERITH_QVGE Design and Testing System. A STATE DIAGRAM mealy machine specification is compiled into C++ code that describes a runtime monitor to be executed in the runtime monitoring tester YRI-DB-RUNTIME-VERIF. Figure 4 depicts a sample State Diagram Mealy Machine specification on a NOT DESIRABLE SQL call sequence. 5.1 HOW TO READ A "SDMM" Figure 1shows a finite automaton representation of the mealy machine description in Figure 4. It shall be read as follows: •Theprogramisinastartstate D; state Disa start state since there is incoming "START" arrow into it. •(Pre-) Condition Q0: "department name ’YRI_ASSET’ is not in table column ’department_name’ of database table ’department’"; applies in state D. •Whenever GUARD CONDITION : in_sql_event_log(’DELETE.department.YRI_ASSET’, STATE(d)): "event’DELETE.department.YRI_ASSET’ appears in SQL event log (trace) leading to state D"; applies in state D, system under test (SUT) event ’SELECT.department’ could occur. •When SUT event ’SELECT.department’ occurs, SUT is now in state E; state Eis an error state because the node that represents it in Figure 1has 2circles on it. •(Post-) Condition Q1: "department name ’YRI_ASSET’ is in table column ’department_name’ of database table ’stocks’"; applies in state E. Thisshall notbethe casesince department ’YRI_ASSET’ isnomoredefinedin SUT database table ’department’. 5.2 "SDMM" WITH MORE THAN 2STATES State Diagram Mealy Machines (SDMM) with more than 2 states have following characteristics, as detailed in scientific and engineering journal paper [Nou23] in preparation: •Only the first transition has a pre-condition specification •Each other transition only has a post-condition specification •Since each state only has 1outgoing state transition, the post-condition of the previous (incoming) state transition acts as the pre-condition of the next transition. 6 YERITH_QVGE (YRI_QVGE) Workflow Figure 10: Workflow explanation. user project directory: "$USER_PROJECT_DIR/sd−mealy−machine−specs". copy ".spec_sd_mealy" generated file into YRI−DB−RUNTIME−VERIF YRI−DB−RUNTIME−VERIF Instrument SUT (system uder test) with QtDbus calls to safety property with YRI_QVGE. draw SQL temporal GENERATE A SINGLE yri−db−runtime−verif executable "$YRI−DB−RUNTIME−VERIF". using bash scripts in folder The "Design and Testing System" YERITH_QVGE works with following workflow, as illustrated graphically in Figure 10, and in Figure 5: 1. Draw Structure Query Language (SQL) temporal safety property using drawing tool YERITH_QVGE; 2. copy the generated ".spec_sd_mealy" files into a user project directory in YRI-DB-RUNTIME-VERIF home development folder: "$YRI–DB–RUNTIME–VERIF"; 3. follow the steps described in Section 7so to gather a single executable that defines all specified runtime monitors. 7 Custom User Project (YRI–DB–RUNTIME–VERIF) Table 3: YRI-DB-RUNTIME-VERIF Directories Variable for illustration purposes Meaning $YRI–DB–RUNTIME–VERIF root directory of YRI-DBRUNTIME-VERIF $YRI–DB–RUNTIME–VERIF/$USER_PROJECT root directory of user project Table 3illustrates directories that will be used to describe a process to generate a single binary executable for a user’s custom project with several runtime monitor specifications. Figure 7illustrates a screenshot of the Graphical User Interface (GUI) of YRI-DB-RUNTIME-VERIF. You can get a copy of YRI-DB-RUNTIME-VERIF using the following command: git clone https://www.github.com/yerithrd/yri-db-runtime-verif Creating a binary executable for State Diagram Mealy Machine (SDMM) specifications consists of the following elements: Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "7 / 10". | Version of – June 7, 2025 – YERITH_QVGE user’s guide YERITHr&d 1. ’MariaDB’ database connection configuration file: this file defines settings to connect to the system under test (SUT) application database; it is located in path: "$YRI–DB–RUNTIME– VERIF/YRI-DB-RUNTIME-VERIF-GUI-ELEMENTS-SETUP/yri-db-runtimeverif-database-connection.properties". A database connection to the SUT application database is required in order to check LTL property through the SDMM application library YRI_SD_RUNTIME_VERIF_LANG. 2. Property configuration file: this file defines environment variables necessary for building a binary executable for the user; it is located in path: "$YRI–DB–RUNTIME– VERIF/$USER_PROJECT/bin/configuration-properties.sh". 3. "$YRI–DB–RUNTIME–VERIF/$USER_PROJECT/sd-mealy-machine-specs": this directory contains user defined State Diagram Mealy Machine (SDMM) specifications to generate Corresponding runtime monitors within a single binary executable. 4. Generate an executable for a user defined runtime monitor: a) A following command MUST be renewed each time you are new in a bash–shell environment; execute following command in directory "$YRI–DB–RUNTIME–VERIF": . ./YRI-create-executable-for-user-SDMM.sh -d $USER_PROJECT b) modify the LTL verification code part within the generated source code files. Then execute following command in directory "$YRI–DB– RUNTIME–VERIF": ./yr_db_runtime_verif_BUILD_DEBIAN_PACKAGE.sh c) uninstall YRI-DB-RUNTIME-VERIF with following command in directory "$YRI–DB–RUNTIME–VERIF": ./yr_DB_RUNTIME_VERIF_uninstall.sh d) re–install YRI-DB-RUNTIME-VERIF with following command in directory "$YRI–DB–RUNTIME–VERIF": ./yr_DB_RUNTIME_VERIF_INSTALL.SH e) Redo [1st–step] in case you add or modify a ’.spec_sd_mealy’ specification file in folder "$YRI–DB– RUNTIME–VERIF/$USER_PROJECT/sd-mealy-machine-specs" ! 8 HOW TO START YRI-DB-RUNTIME-VERIF •The "ELF-x64" binary executable, in the source development directory is located in full path: "$YRIDB-RUNTIME-VERIF/bin". •The DEBIAN–LINUX icon ( ) of YRI-DB-RUNTIMEVERIF is located in "Applications" menu under section "Programming", and section "Accessories". •The "ELF-x64" binary executable, after installation of the DEBIAN–LINUX package ’yri-db-runtime-verif.deb’ is located in full path: "/opt/yri-db-runtime-verif/bin". Figure 11: SAMPLE sql recovery state diagram model in YERITH_QVGE 9 SQL QUERY Recovery execution on demand A user can specify which SQL command query to execute whenever a System Under Test (SUT) lands in an accepting error state. This is done using keywords ending with "AUTO", used for meaning "AUTO RECOVERY FROM FAIL STATE": 1. recovery_sql_query 2. END_STATE_AUTO 3. FINAL_STATE_AUTO 4. ERROR_STATE_AUTO. The use of an "AUTO" keyword shall be accompanied with a use of keyword recovery_sql_query, that specifies a SQL command query to run when landing in this fail error accepting state. 9.1 Automatic SQL Command Query Generation YERITH_QVGE implements an automatic SQL query generation strategy incasea userdon’tspecify aSQLcommand query, sinceit could be leaved empty: Subsections 9.1.1,9.1.2,9.1.3, and 9.1.4 describe the strategy implemented. Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "8 / 10". | Version of – June 7, 2025 – YERITH_QVGE user’s guide YERITHr&d 9.1.1 ERROR ACCEPTING STATE for sdmm 1. not in_before (YX,YY)ACTION (V) in_after (DD,YR) 9.1.2 RECOVERY 1. in_after (DD,YR)ACTION (RECOVERY_ND) not in_after (DD,YR) 9.1.3 RECOVERY 2 (Practical solution to be implemented in YRI-DB-RUNTIME-VERIF. in_after (DD,YR)ACTION (RECOVERY_D) in_after (YX,YY) 9.1.4 Concrete RECOVERY 2 action. in_after (YX,YY)insert_RECOVERY (YX,YY) in_before (YX,YY)• 10 HOW TO USE a user interface Figure 12: YERITH_QVGE user interface screenshot. 11 YRI_SD_RUNTIME_VERIF SPECIFICATION LANGUAGE Figure 13 illustrates a ”Backus-NAUR form (BNF)” of our specification language for YRI-DB-RUNTIME-VERIF tool. 12 Formal Scientific and Engineering Project Description Detailed formal scientific and engineering contributions of design and testing system YERITH_QVGE can be found in JOURNAL ARTICLE "Runtime Verification Of SQL Correctness Properties with YRI-DB-RUNTIME-VERIF" [Nou23]. 13 Conclusion The graphical drawing tool YERITH_QVGE (Figure 6) costs only 2, 500 EUROS. WE ONLY SUPPORT DEBIAN–LINUX (https: //www.debian.org). References [Nou23] Xavier Noundou. A Framework for Verifying SQL Correctness Temporal Properties of [GUI] Software at Runtime. https://zenodo.org/records/ 13232567, October 2023. Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "9 / 10". | Version of – June 7, 2025 – YERITH_QVGE user’s guide YERITHr&d Figure 13: Grammar in Backus–Naur Form (BNF) of YRI_SD_RUNTIME_VERIF_LANG Mealy Machine STATE DIAGRAM Specification Language. 〈specification〉::= yri_sd_mealy_automaton_spec ’{’ 〈mealy-automaton-spec〉’.’ ’}’ 〈mealy-automaton-spec〉::= 〈sut-state-spec〉 |〈sut-state-spec〉’→’〈sut-edge-state-spec〉 〈sut-edge-state-spec〉::= 〈sut-edge-mealy-automaton-spec〉’→’〈mealy-automaton-spec〉 〈sut-edge-mealy-automaton-spec〉::= 〈edge-mealy-automaton-guard-cond〉 〈event-call〉 〈edge-mealy-automaton-guard-cond〉::= /* empty */ ’/’ | ’[’ 〈trace-specification〉’]’ ’/’ 〈trace-specification〉::= 〈in-sql-event-log〉|〈not-in-sql-event-log〉|〈in-set-trace〉|〈not-in-set-trace〉 〈sut-state-spec〉::= 〈start-state-property-spec〉 |〈start-state-property-spec〉’:’ 〈algebra-set-specification〉 |〈state-property-spec〉’:’ 〈algebra-set-specification〉 |〈final-state-property-spec〉’:’ 〈algebra-set-specification〉 |〈final-state-auto-property-spec〉’:’ 〈algebra-set-specification〉’:’ 〈recovery-sql-query-spec〉 〈algebra-set-specification〉::= 〈in-algebra-set-spec〉|〈not-in-algebra-set-spec〉 〈in-algebra-set-spec〉::= 〈in-spec〉’(’ 〈prog-variable〉’,’ 〈db-table〉’.’ 〈db-column〉’)’ |〈in-spec-nop〉’(’ ’)’ 〈not-in-algebra-set-spec〉::= 〈not-in-spec〉’(’ 〈prog-variable〉’,’ 〈db-table〉’.’ 〈db-column〉’)’ |〈not-in-spec-nop〉’(’ ’)’ 〈in-sql-event-log〉::= in_sql_event_log’(’ 〈event-call〉’,’ 〈state-property-specification〉’)’ 〈not-in-sql-event-log〉::= not_in_sql_event_log’(’ 〈event-call〉’,’ 〈state-property-specification〉’)’ 〈in-set-trace〉::= in_set_trace’(’ 〈event-call〉’,’ 〈state-property-specification〉’)’ 〈not-in-set-trace〉::= not_in_set_trace’(’ 〈event-call〉’,’ 〈state-property-specification〉’)’ 〈in-spec〉::= IN_BEFORE |IN_AFTER |IN_PRE |IN_POST 〈in-spec-nop〉::= IN_POST_NOP 〈not-in-spec〉::= NOT_IN_BEFORE |NOT_IN_AFTER |NOT_IN_PRE |NOT_IN_POST 〈not-in-spec-nop〉::= NOT_IN_POST_NOP 〈start-state-property-spec〉::= START_STATE’(’ AlphaNum ’)’ 〈state-property-spec〉::= STATE’(’ AlphaNum ’)’ 〈final-state-property-spec〉::= END_STATE’(’ AlphaNum ’)’ | FINAL_STATE’(’ AlphaNum ’)’ | ERROR_STATE’(’ AlphaNum ’)’ 〈final-state-auto-property-spec〉::= END_STATE_AUTO’(’ AlphaNum ’)’ | FINAL_STATE_AUTO’(’ AlphaNum ’)’ |ERROR_STATE_AUTO’(’ AlphaNum ’)’ 〈recovery-sql-query-spec〉::= recovery_sql_query’(’ 〈db-table〉’,’ 〈sql-recovery-query〉’)’ 〈sql-recovery-query〉::= String 〈event-call〉::= String 〈prog-variable〉::= AlphaNum 〈db-table〉::= AlphaNum 〈db-column〉::= AlphaNum Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "10 / 10". | Version of – June 7, 2025 –