GROUPED DOCUMENTS as SOFTWARE ARCHITECTURE DESCRIPTION of YEROTH-ERP-3.0

YERITH_QVGE 2 YERITH-ERP-9-0-SOFTWARE-SYSTEM-ARCHITECTURE 42 YERITH-ERP_multi_sites_base_de_donnees 79 yri-sd-db-runtime-verif 98 YERITH_QVGE-intro 2 YERITH_QVGE-definitions---cheat--sheet 6 YERITH_QVGE-user-guide 27 YERITHr&d |information brochure of YERITH_QVGE Information Brochure of the Design and Testing System YERITH_QVGE (YRI_QVGE) Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] CONTACT: [email protected] Table 1: EQUIVALENCES scientific literature engineering acronym PRE BEFORE POST AFTER A TRACE AN EVENT LOG A FINAL STATE AN ERROR STATE 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: A SAMPLE state diagram mealy machine file. KEYWORDS belonging both to ’engineering (ERROR_STATE)’, 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. } Figure 3: A SCREENSHOT OF YERITH_QVGE. Figure 4: A SCREENSHOT OF YRI-DB-RUNTIMEVERIF SQL EVENT LOG. Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page 1. | Version of – October 14, 2025 – YERITH_QVGE: a design tool for testing sql correctness properties YERITHr&d 1 Developer Biography Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] is a CHRISTIAN BY FAITH, Cameroonian, born on September 16 1983 in DOUALA (LITTORAL region, CAMEROON). Xavier has a ”Diplom– Informatiker (Dipl.–Inf.)” qualification from the University of Bremen, Bremen, Bremen, GERMANY (May 25,2007). XAVIER NOUNDOU IS A ”Dr.–Ing. :Doctor of Engineering (PhD equivalent – Computer Software Verification & Analysis)”from THE UNIVERSITY OF WATERLOO (ON, CANADA); DECEMBER 20, 2011 ! Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] has worked together with Pr. Prof. Dr. habil. Jan Peleska, at AGBS– University of Bremen, GERMANY; and 2years later at WatForm– University of Waterloo, ON, Canada, with Pr. Prof. Dr.–Ing. Patrick Lam. Xavier could successfully work with Dr. Frank Tip at The University of Waterloo (Waterloo, ON, Canada) on his first JAVA dynamic program analysis. Xavier also had the great opportunity through Pr. Prof. Dr.–Ing. Marcel Mitran and Pr. Prof. Dr.–Ing. Patrick Lam; to work as a graduate intern in Markham (Toronto, ON, CANADA) at IBM TORONTO SOFTWARE LABORATORY; in the JAVA–J9 Just–In–Time Compiler Optimization Team, together with Vijay Sundaresan, M.Sc. (McGill University, QC, Canada). Xavier has following academic and professional engineering research contributions: 1. ’Statistical test case generation for reactive systems’ at RTT-MBT at VERIFIED SYSTEMS INTERNATIONAL GmbH (https://www.verified.de). 2. ’Context-Sensitive Staged Static Taint Analysis For C using LLVM’: 1. source code in C++: https://www.github.com/sazzad114/saint 2. full text: https://zenodo.org/record/8051293 . 3. ’YERITH-ERP-3.0’: 1. source code in C++: a. YERITH–ERP–9.0: https://www.github.com/yerithrd/ yerith-erp-9-0 b. YERITH–ERP–9.0 SYSTEM DAEMON: https://www.github.com/yerithrd/ yerith-erp-9-0-system-daemon 2. full text (ongoing publication): https://zenodo.org/record/8052724 . 2 Introduction Figure 5: SOFTWARE ARCHITECTURE OF YRI-DBRUNTIME-VERIF. OPERATING SYSTEM (OS) MYSQL library methods calls OS system calls yri−db−runtime−verif QT socket calls (via Qt−Dbus) A RUNTIME MONITOR LIBRARY − PLUGIN PUA / SUT (JVM−java virtual machine) PUA source code instrumented YERITH_QVGE is a CASE (Computer-Aided Software Engineering) design tool to generate "domain-specific language (DSL) YRI_SD_RUNTIME_VERIF_LANG 1" files, to be inputted into the "compiler YRI_SD_RUNTIME_VERIF_LANG_COMP", so to generate C++ files for the runtime verifier tester "YRI-DBRUNTIME-VERIF 2" that allows for manual verification of SQL correctness properties of Graphical User Interface (GUI) software. YRI-DB-RUNTIME-VERIF inputs SQL correctness properties expressed using the formalism state diagram mealy machine (YRI_SD_RUNTIME_VERIF_LANG). Figure 5illustrates a software system architecture of YRI-DB-RUNTIME-VERIF, together with the monitored program under analysis. The Free Open Source Code Software (FOSS) tool-chain of development testing is located as follows for free, EXCEPT for "YERITH_QVGE " that is a Closed Source Code Software (CSCS): •COMPILER (i.e.: YRI_SD_RUNTIME_VERIF_LANG_COMP): https://www.github.com/yerithrd/yri_sd_runtime_ verif_lang •RUNTIME VERIFIER TESTER (i.e.: YRI-DB-RUNTIME-VERIF): https://www.github.com/yerithrd/ yri-db-runtime-verif •state diagram mealy machine UNIT TESTS CODE (i.e.: YRI_SD_RUNTIME_VERIF_UNIT_TESTS): https://www.github.com/yerithrd/yri_sd_runtime_ verif_UNIT_TESTS •state diagram mealy machine (i.e.: YRI_SD_RUNTIME_VERIF_LANG): https://www.github.com/yerithrd/yri_sd_runtime_ verif 3 YERITH_QVGE (YRI_QVGE) Project Dependency Table 2: YERITH_QVGE Design and Testing System Dependencies 1https://www.github.com/yerithrd/yri_sd_runtime_verif_lang 2https://www.github.com/yerithrd/yri-db-runtime-verif Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page 2. | Version of – October 14, 2025 – YERITH_QVGE: a design tool for testing sql correctness properties YERITHr&d PROJECT Required 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. Figure 6: YERITH_QVGE software library dependencies. YRI_SD_RUNTIME_VERIF_LANG YRI_SD_RUNTIME_VERIF_LANG_COMP YRI_SD_RUNTIME_VERIF_UNIT_TESTS Runtime monitor container (e.g.: YRI−DB−RUNTIME−VERIF) Design SDMM; from CASE tool (e.g.: YERITH_QVGE) Figure 6show a diagram overview of the presentation in Table 2. The step of the unit tests is colored in gray because it is only for developers of YERITH_QVGE intended. 4 Potential Uses of YERITH_QVGE YERITH_QVGE (YRI_QVGE) could be used for the following automatic generation, analysis, verification, and validation tasks: 1. Automatic generation of runtime monitoring module program to prove whether a test procedure, automated, or not, is correct with regards to a test and / or design STATE DIAGRAM MEALY MACHINE. In effect, let the test execution be runtime monitored to watch whether accepting error states would be found. For instance, Junit testing environment could automatically integrate an automatically generated runtime monitor infrastructure for unit testing. 2. Automatic generation of runtime monitoring module program for any software that can emit DBus messages. Such runtime monitoring modules are for interest for special LTL model checking properties that cannot get a definite answer through use of a conventional model checker. 3. Software design properties with SQL 4. Software design properties including event sequences over different layers of software system architecture 5. Class diagram with sequence diagram. 5 Advantages of YERITH_QVGE Figure 7: Workflow. 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 A sample state diagram mealy machine is shown in Figure 2. 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_COMP) do it for you. 6 Conclusion YERITH_QVGE costs only 2, 500 EUROS. WE ONLY SUPPORT DEBIAN–LINUX (https://www.debian.org). Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page 3. | Version of – October 14, 2025 – Index state diagram mealy machine, 2 CASE (Computer-Aided Software Engineering), 2 domain-specific language (DSL), 2 runtime verifier tester, 2 SQL correctness properties, 2 4 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 11 3.1 Development Toolchain ................................................................ 11 4 METHODS of C++ Library ”YRI_SD_RUNTIME_VERIF”12 4.1 Generated Method YOU need to code ....................................................... 12 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 – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d List of Figures 1 A motivatingexample, as previousbug foundin 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 INTERNET-RELATED 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 – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d 1.4 State Diagram Mealy Machine : Usages & Advantages 1.4.1 Usages ◦Software code program testing & verifying requires means of expressing requiring in a form that can be used and executed by a computer program. "SDMM " is a textual (See Figure 4) and graphical (See Figure 1) representation of software system requirements; HOWEVER, requirements expressed using "SDMM " are fail (forbidden) requirements : I.E., software system execution run that shall never happen ! ◦During software development, developers need to characterize effects of program statements onto software program behavior. For instance, what causes the deletion of a database table column department value at the level of the software user– scale (Example in Figure 2). Figure 2could also be represented by a state diagram mealy machine as illustrated in Figure 1. 1.4.2 Advantages ◦WHITE-box as Well As Black-box testing is possible and / or available at once for any developer in testing; Depending on how YOU specify your runtime monitoring diagram & code (See Section 4.1). ◦Software developers could implement code source checking of LTL–model checking formulas (https: //www.wikipedia.org/)fortheirfail (forbidden) program requirements; I hope to also have sample LTL–model checking formulas implemented in future releases of YRI-DB-RUNTIME-VERIF, which is a runtime monitoring verification container provided to work with the "YRI_QVGE Design & Verification System". ◦Software developers that create & maintain fail (forbidden) program requirements mustn’t have a perfect knowledge of code sources of the System Under Test. 1.4.3 Cases of Practical Usages of ”SDMM” ◦Automobile industry ”car–automobile–breaking safety & security usage rules” on–the–fly to avoid thousands of car–recall because of a bug (E.g.: Toyota Camry 2009 (https://https://en.wikipedia.org/wiki/ 2009%E2%80%932011_Toyota_vehicle_recalls)); A car defect could only just be fixed at any Toyota registered auto-car-dealer by inputting a ”SDMM” fix specification into an in–car placed YRI–QVGE–PC–Tablet device; Instead of sending it back to a Toyota car factory ! 1.5 State Diagram Mealy Machine : Brief Summary Explanation "YRI_SD_RUNTIME_VERIF" has following usages and advantages: I.)Formalism STATE DIAGRAM mealy machine for system specification: Mealy Machines are kind of state machines where output states depend only on input on a source state. STATE DIAGRAM mealy machine as defined by myself is a finite state automaton that only has following characteristics: a.) Each automaton / machine only has 1start state S0, and 1final state Sfthat is an accepting / error state. A final, accepting, or error state is a state that shows a defect status of the system under analysis (SUA / PUA / SUT). b.) Each state Sionly has 1outgoing state transition to an output state S0. c.) Each transition T, except a start transition ”start”, could havea pre-condition,andpost-condition; That bothare called or named state-edge-condition (pre-condition on T1:”T1”; post-condition on T1:”T1”). A state Sihas a state–condition either as precondition ”T1” on a state transition Or as a post– condition ”T1” of a state transition T1. In Figure 1, state–conditions are for instance ”Q0”, and ”Q1”. Each state–condition ”Si”, and / or pre–condition; And / or post–condition is an algebra set specification that uses set inclusion operations : ∈,/∈. d.) A set inclusion operation as state–condition for a state Sicould for instance be : 1.)Q0 :=IN_BEFORE(y, D) is to read “BEFORE next event, variable yis IN set D(y∈D)“. THIS boolean first–order preposition is assigned into variable Q0; the ”underlining” illustrates that this is a pre–condition : ”meaning a condition That shall hold before (PRE) next event to occur in software system.” 2.)Q0 :=IN_AFTER(y, D) is to read “AFTER next event, variable yis IN set D(y∈D)“. THIS boolean first–order preposition is assigned into variable Q0; the ”over-lining” illustrates that this is a post–condition : ”meaning a condition That shall hold after (POST) next event to occur in software system.” 3.)IN_BEFORE_NOP() : THIS boolean first–order preposition means that this pre–condition (’True’) holds before (BEFORE) next event to occur in software system.” 4.)IN_AFTER_NOP() : THIS boolean first–order preposition means that this post–condition (’True’) holds before next event to occur in software system, after (POST) previously occurred event.” 5.)NOT_IN_BEFORE(y, D) 6.)NOT_IN_BEFORE_NOP() 7.)NOT_IN_AFTER(y, D) 8.)NOT_IN_AFTER_NOP() I I.)AC++ library that implements runtime monitoring and fail–state recovery as a static library : (https: //www.github.com/yerithrd/yri_sd_ runtime_verif). III.)A Free and OPEN SOURCE CODE SOFTWARE (Foss) implementation of a runtime monitor for using state diagram mealy machine specifications; BY means of a QT–dbus software communication stack with your own software : ”YRI-DB-RUNTIMEVERIF”(https://www.github.com/yerithrd/ yri-db-runtime-verif). YRI_SD_RUNTIME_VERIF’s formal description of the state diagram formalism follows Mealy machine [Wik22] added with accepting states (final or erroneous states), and state diagram transition preand post-conditions : ”state diagram mealy machine” ("SDMM"). Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "7 / 16". | Version of – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Another excellent, detailed with proofs and theory presentation of mealy automata [PlH21] is available. In comparison to statechart [HarXX], which is a visual formalism for states diagrams, YRI_SD_RUNTIME_VERIF doesn’t support at time for instance the following features: hierarchical states (composite state, submachine state), timing conditions. A sample state diagram mealy machine is pictured in Figure 1. Dis the start state, 1.6 Related State Diagram Formalisms We here cite sample state diagram formalisms and the theory behind them for checking and / or verifying software design & programming properties. ◦Statechart by David HAREL : A statechart is here a visual formalism–description to enable a description of a complex software system that can also have states with substates; And / or timing conditions on states entries, and / or transition triggering conditions. ◦”Kripke structure” with THEORY & formalism called ”MODEL Checking”; mainly by DAVID–Emerson & CLARKE– Edmund [CGK+18](https://mitpress.mit.edu/ books/model-checking-second-edition) Software tools to perform model checking are called model checkers. Sample model checkers are NuSMV (https: //nusmv.fbk.eu/downloads.html); SMV (https: //mcmil.net/smv.html); Spin-model checker (https://spinroot.com/spin/whatispin.html). 1.6.1 David Harel Statechart : A Visual Formalism for State Diagram Figure 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”—. entry / PostEvent(’DELETE.dept.YRI_ASSET’) dept_exits dept_exists’ entry / PostEvent(’SELECT.stocks’) ’SELECT.dept’ ’SELECT.stock’ Statechart[HarXX], as defined andproposed byDavid HAREL; Represent diagrams, sometimes composite with internal states that are used to describe reactive systems, meaning systems that react and act based on environmental input and interaction. QT development library professional supports statechart as defined by David-Harel. SCXML is used to specify a state machine. (https://www...) Timed Discrete Input / Output Hybrid System (TDIOHS) as defined by Peleska et al. [BFPT06] implements David-HAREL statechart full compatibility incorporating the following elements for software system specification & elicitation : 1.)Asoftware system behavior and actions can be represented as finite set of configurations; A configuration is an assignment of variables to values that situates a software system evolution over time; 2.)A set of configurations of a software system as a finite states graphrepresentation wherenodesrepresentsoftwaresystem states, And edges represent transition between software system states; 3.)Start– & End– (Final–, Accepting–, Erroneous–) state to represent INITIAL & FINAL software system state. A reactive system has a particularity that it doesn’t define a final-accepting state as it continuously reacts with its environment : it loops around its start state; 4.)Software system states transition defined as graph–edge between software system configuration–states; 5.)Software system state transition ”Event” as label between graph–nodes; 6.)Guarded condition as behavioral condition that must hold in order for a state transition event to trigger & thus send the software system into a new configuration; 7.)Timing condition 8.)hierarchical states (composite states, submachine state) 1.6.2 Timed Discrete Input / Output Hybrid System (TDIOHS) Figure10: A STCT–symbolic testcasetree randomly generatedby manual drawing for explanation purposes. 0N TDIOHS–Timed-Discrete-Input-Output-HybridSystem [BFPT06] is a statechart compatible state diagram formalism defined by "Peleska et al." at the University of Bremen in Germany. "Peleska et al." define a test mechanism to generate test cases from TDIOHS statechart visual description; The generated test cases abide to "Marie–Claude Gaudelle" algorithm defined in [Gau06] to statistically and uniformly-distribute test cases around a tree that describe all potential program code execution paths : STCT (Symbolic Test Case Tree). A System Under Test (SUT) tree execution paths could then be traversed based on the real test data generated by a symbolic test data generator component as illustrated for instance in [nf10]. A sample STCT is illustrated in Figure 10; ”N0” is a start node of the program tree. 1.6.3 TDIOHS in Action within ”Borland Together 6”with RT– Tester of ’verified.de’ Xavier NOUNDOU, myself, wrote together with Verified Systems International GmbH a plugin that enables developers to automatically create C++ testing code for design drawings created in the CASE-Computer Aided Software Engineering Design tool Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "8 / 16". | Version of – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d ”Borland Together 6”(https://en.wikipedia.org/ wiki/Micro_Focus_Together) . I performed this task under supervision and advising of ”Jan Peleska”, as a student in Computer Science at the University of Bremen in Bremen–Germany in years ”2004 /2005”. Based on the automatically generated C++ module code, a developer could then use the UNIT Testing Framework for embedded systems RT-Tester of Verified.de (https://www.verified.de/products/ model-based-testing) to create software module unit testing code with following criteria : 1.)MCDC (Modified Condition Decision Coverage) : test cases & data for checking any outcome of any boolean assignment of variables involved & used in a conditional IF-Then-Else branching statement; 2.)Uniformly statistically distributed test cases [NN07] & test data [nf10] from all possible test runtime execution of the Program Under Analysis (PUA) [NN07,BFPT06]; 3.)Myself I only received "2, 000 Euros" as fund collected as money–rewards–intellectual property out of this work since ”May 2007” when I delivered program code software as part–deliverable to acquire my ”Diplom–INFORMATIKER” qualification from the department of Mathematics & Computer Science (”Fachbereich 3”) of the ”UNIversity– racist of Bremen–Germany”. 1.6.4 TDIOHS in Action by ”Automatic Test Cases / Data Generation” Master Thesis [NN07] in Computer Science of ”Xavier N. NOUNDOU”, at the University of Bremen in Bremen–Germany; demonstrates an implementation of uniform distributed statistically algorithm for selecting paths for creating test cases from a Statechart designed in ”Borland-Together 6”. The statechart is first of all transformed into a Symbolic Test Case Tree (STCT) before ”MARIE-Claude Gaudelle” [Gau06] modified algorithm by [NN07] is applied. In [CHKS12], Tatiana Mangels & Jan Peleska present "CTGEN", a Unit Under Test (UUT) test cases and test data generator for embedded system writen in the Cprogramming language. More information and contacts for buying and / or trying this software product can be found at following URL : https://www.verified.de/products/model-based-testing, from the German society ”Verified Systems International GmbH”. 2 Mathematical Formal Definition of SDMM THIS section gives a mathematical theoretical definition of state diagram mealy machine (abbreviated ”SDMM”), as conceived originally by us for our project YERITH–ERP–9.0 [Nou22] runtime monitoring verification started in year 2015 in Yaounde Cameroon. YRI_SD_RUNTIME_VERIF’s formal description of the state diagram formalism follows Mealy machine [Wik22] added with accepting states (final or erroneous states), and state diagram transition preand post-conditions: ”state diagram mealy machine”. Another excellent, detailed with proofs and theory presentation of mealy automata [PlH21] is available. In comparison to statechart [HarXX], which is a visual formalism for states diagrams, YRI_SD_RUNTIME_VERIF doesn’t support at time for instance the following features: hierarchical states (composite state, submachine state), timing conditions. 2.1 Definition 1: A state diagram (for mealy machine). A state diagram is an 8–tuple (S,S0,C,Σ,Λ,δ,T,Γ)where: •S: a finite set of states •S0∈S: a start state (or initial state) •C: a set of predicate conditions; pre-conditions are underlined (e.g.: Q0), and post-conditions are overlined (e.g.: Q1). A pre-condition is comparable to a Harelstatechart guarded condition. •Σ: an input alphabet, Σ:= {False,True}. ′False′means no input from SUT into YRI-DB-RUNTIME-VERIF. ′True′means any input could come from SUT. •Λ: an output alphabet (of program events en(n∈N)), φthe no program event. A program event generally corresponds to a function or method call at a SUT source code statement (or program point). •δ:S×C: a 2-ary relation that maps a state sto a state-condition cas either a state diagram transition precondition(c), or as astate diagramtransition post-condition (c). •T:S×Σ→S×Λ: a transition function that maps an input symbol to an output symbol and the next state. •: a 2−ar y relation that maps a state diagram transition to a guarded condition expression. •Γ: a set of accepting states; Γ∈S. For instance, for the motivating example described in Figure 1 we have: •S={D,E}; •S0=D; •C={Q0,Q1}; •Σ={False,True}; •Λ={φ,’SELECT.department’}; •δ={(D,Q0),(E,Q1)}; •T={((D,False),(D,φ)),((D,True),(E,’SELECT.department’))}; •Γ={E} 2.2 Definition 2: A pre-condition. A pre-condition of a state diagram transition is a predicate hat must be true before the transition can be triggered. A precondition Q0could have 2forms: •Q0:=IN_PRE(X, Y) that means value "X" is in (∈) database column value set "Y". •Q0:=NOT_IN_PRE(X, Y) that means value "X" is not in (/∈) database column value set "Y". 2.3 Definition 3: A post-condition. A post-condition of a state diagram transition is a predicate that must be true after the transition was triggered. A post-condition Q1could have 2forms: •Q1 :=IN_POST(A, B) that means value "A" is in (∈) database column value set "B". •Q1 :=NOT_IN_POST(A, B) that means value "A" is not in (/∈) database column value set "B". For state diagram mealy machines with more than 2states, only the first transition has a pre-condition specification (IN_PRE, or NOT_IN_PRE). Each other transition only has a post-condition specification (IN_POST, or NOT_IN_POST). Since each state only has 1outgoing (edge) state transition, the post-condition of the Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "9 / 16". | Version of – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d previous (incoming) state transition acts as the pre-condition of the next transition. IT is also for user interest to have following NO–OPeration post-conditions when working with state diagram mealy machines with more than 2states : ◦IN_POST_NOP ◦NOT_IN_POST_NOP OUR experience, not reported at time anywhere, shows that state diagram mealy machine with more than 2states are really more for parallel system modeling; I.E. systems that work in GUI with timers and several threads of work at anytime. “In such cases, subsequent linearly placed states may not belong to same thread of execution: this is kind of what is called in CSP (Communicating Sequential Processes) []; Parallel Composition.“ Subsection 2.7 details better and well this corelation between ”CSP” [Ra01] & ”SDMM”. 2.4 Definition 4: A trace. A trace Tn=<e0,e1, .., en>is a sequence of SUT events (or SUT program points) ei,i∈{0,..,n}of length n.trace(D)is the trace of SUT events up to state D. For instance, for the motivating example described in Figure 1we have: t race(E) = trace(D),< ’SELECT.department’>. 2.5 SUT Event Processing Method YRI_trigger_an_edge_event Listing 2illustrates the pseudo–code of YRI_SD_RUNTIME_VERIF SUT event processing method YRI_trigger_an_edge_event(QString an_edge_event). ’YRI_trigger_an_edge_event(QString an_edge_event)’ is responsible for interpreting a monitor at runtime, based on its current state, and on the current event received from SUT. Each state in YRI_SD_RUNTIME_VERIF states diagrams shall have only 1 outgoing edge (transition), by specification and construction, as explained in Proposition 2.5.1 in Section 2. The algorithm in Listing 2demonstrates that, given correct trace and event information from SUT, YRI_SD_RUNTIME_VERIF always exactly matches the user specification. Thus never giving false warnings. 2.5.1 Proposition 1: NO FALSE WARNINGS. YRI_SD_RUNTIME_VERIF only allows 1outgoing edge or transition for a state in its specifications, and for not desirable (forbidden) behavior, as illustrated in Figure 1. These 2properties, together with algorithm ’YRI_trigger_an_edge_event(QString an_edge_event)’ (Listing 2) of YRI_SD_RUNTIME_VERIF, ensures that there are no false warnings during YRI-DB-RUNTIME-VERIF analyses. For example, the opponents runtime monitoring and / or verification tools–systems [BH12,BRBY00,AAC+05,Bod05, CR07] may give false warnings. We need to also report that if a developer doesn’t well specify to the runtime verifier tester where to emit event, as for instance in ”Listing 1”, false warnings (false positives) may occur. 2.5.2 Explanation on HOW to avoid code that creates False Warnings (False Positives) 2.6 Guarded Condition Expression Specification in YRI_SD_RUNTIME_VERIF Guarded conditions expressions can be specified using one of the yr_create_monitor_edge method and a boolean expression of type YR_CPP_BOOLEAN_expression. An edge without an explicit guarded condition has an implicit ’[True]’ guarded condition on it. The implicit guarded condition ’[True]’ mustn’t be identified as an implicit input event ’True’, as specified in Definition 1. Guarded conditions are meant to be trace set specification on program events. For instance in Figure 1(motivating example): "[in_set_trace (’DELETE.department.YRI_ASSET’, STATE(D))]"means that a SQL ’DELETE’ event removing a department named ’YRI_ASSET’ from MariaDB SQL table ’department’ must have occurred in the trace leading to state ’D’, before event ’SELECT.department’ can be triggered. A guarded condition could have two practical forms: •"[in_set_trace (’event’, STATE(D))]" is equivalent to: ’event’ ∈trace(D). •"[not_in_set_trace (’event’, STATE(D))]" is equivalent to: ’event’ /∈trace(D). where ’event’ is an input event (event ∈Σ) and ’D’ a state diagram state (D∈S). 2.7 SDMM for modeling parallel-concurrent software system A state in an state diagram mealy machine specification acts as a parallel concurrent process state. IT means each state transition represents a parallel– concurrent process synchronization event as for example defined in a formalism named CSP (Concurrent Sequential Processes) as a parallel composition operator ("||"). For instance, in Fig. 1, Processes D&Ecould be specified in communication in CSP like : ”(D|| B)over event SELEC T.depar tment” ! TODO : improve syntax description of CSP. 2.8 SDMM in Action within YRI_QVGE by ’Yerith R&D’ A screenshot of a fail (forbidden) state diagram mealy machine is illustrated in Figure 6. This fail fail (forbidden) state diagram mealy machine is the same described in Figure 4with ”YRI_QVGE Design & Verification System” domain specific language (DSL) ”YRI_SD_RUNTIME_VERIF_LANG”. The program–DSL code source illustrated in Figure 4was automatically generated by myself by ”Saving a design as a DOT/GraphVIZ” document. ”Savinga designdrawingasa DOT/GraphVIZ” creates source code in domain specific language ”YRI_SD_RUNTIME_VERIF_LANG” within a file ending with ’.sd_mealy’. 2.9 SDMM in Action by automatic ”Runtime Monitors Automatic Generation” I created YRI-DB-RUNTIME-VERIF so to allow automatic generation of runtime execution time monitoring modules for state diagram mealy machine defined using a Domain Specific Language (DSL) called YRI_SD_RUNTIME_VERIF_LANG. YRI_SD_RUNTIME_VERIF enables expression and description of state diagram mealy machine specification. THE Domain–Specific Language (DSL) definition in Backus– Naur–Form (BNF) (https://en.wikipedia.org/ wiki/Backus%E2%80%93Naur_form) of this DSL called YRI_SD_RUNTIME_VERIF_LANG is printed in the USER’S guide of YRIDB-RUNTIME-VERIF (https://www.zenodo.org/records/ 17316481). Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "10 / 16". | Version of – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d Listing 2: C++ Pseudo-code for YRI_trigger_an_edge_event(QString an_edge_event):YRI_SD_RUNTIME_VERIF method for triggering state diagram events (edges or transitions). 1bool MONITOR::YRI_trigger_an_edge_event(QString an_edge_event) 2 { 3 MONITOR_EDGE cur_OUTGOING_EDGE = _cur_STATE.outgoing_edge(); 4 5if (cur_OUTGOING_EDGE.evaluate_GUARDED_CONDITION_expression() && 6 (an_edge_event == cur_OUTGOING_EDGE.edge_event_token())) 7 { 8bool precondition_IS_TRUE = cur_OUTGOING_EDGE 9 .CHECK_SOURCE_STATE_PRE_CONDITION(_cur_STATE); 10 11 if (precondition_IS_TRUE) 12 { 13 set_current_triggered_EDGE(cur_OUTGOING_EDGE); 14 15 MONITOR_STATE a_potential_accepting_state = 16 cur_OUTGOING_EDGE.get_TARGET_STATE(); 17 18 if (CHECK_whether__STATE__is__Final(a_potential_accepting_state)) 19 { 20 CALL_BACK_final_state_FUNCTION(a_potential_accepting_state); 21 } 22 return true; 23 } 24 } 25 return false; 26 } 3 HOW TO Setup C++ Library ”YRI_SD_RUNTIME_VERIF” for Usage in A C++ PROGRAM SOURCE CODE When you build runtime monitoring verification library ”YRI_SD_RUNTIME_VERIF”, a static binary library is newly generated. YOU then need to copy this newly created static binary library into your C++ project. YOU then need for instance using QT, to put a line as follows so to be able to use ”YRI_SD_RUNTIME_VERIF”: LIBS += -L$$PWD/lib_SD -lyri_sd_runtime_verif in your project file ending with following string ’.pro’ (e.g.:qtproject.pro”); Whereas string "-L$$PWD/lib_SD" represents a path that leads to where ”YRI_SD_RUNTIME_VERIF” is stored. String "-lyri_sd_runtime_verif" mentions to link (”-l”) runtime monitoring library ”YRI_SD_RUNTIME_VERIF” during your build process ! 3.1 Development Toolchain Table 2illustrates for each library project, which others it depends on. 1.)The runtime monitoring interface static library ”YRI_SD_RUNTIME_VERIF”enables users to express software program states, that are incorrect, USING mealy machines since mealy machine transitions depends only on the current state and its current input; 2.)”YRI_SD_RUNTIME_VERIF_UNIT_TESTS”is only required in case you modified the FOSS library ”YRI_SD_RUNTIME_VERIF” and would like to apply some unit tests to check your modifications. 3.)The LIBRARY and / or language that enables to specify ”YRI_SD_RUNTIME_VERIF”state diagram mealy machines is called ”YRI_SD_RUNTIME_VERIF_LANG”; 4.)The LIBRARY that creates for you the incorrect mealy machine as a C++ code, by describing it using either a text file, and / or a state machine described using YRI_QVGE (”YRI_SD_RUNTIME_VERIF_LANG”) as a design drawings; IS coined the name ”YRI_SD_RUNTIME_VERIF_LANG_COMP”; 5.)NORMALLY you wouldn’t need to directly invoke the compiler / translator ”YRI_SD_RUNTIME_VERIF_LANG_COMP”. This is best done by the runtime monitor generator ”YRI-DBRUNTIME-VERIF”. The user’s guide for ”YRI-DB-RUNTIME-VERIF”(https:// www.zenodo.org/records/17316481) explains how to do so. Table 2: YERITH_QVGE Toolchain PROJECT Required Program / Library 1)YRI_SD_RUNTIME_VERIF ”Qt-trolltech” (https://doc.qt.io/qt-5) 4)YRI_SD_RUNTIME_VERIF_UNIT_TESTS 1) 2)YRI_SD_RUNTIME_VERIF_LANG 1) 3)YRI_SD_RUNTIME_VERIF_LANG_COMP 2) 5)YRI-DB-RUNTIME-VERIF 3) Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "11 / 16". | Version of – October 15, 2025 – YRI_SD_RUNTIME_VERIF :C++ Functional Library for specifying "SDMM"YERITHr&d 4 METHODS of C++ Library ”YRI_SD_RUNTIME_VERIF” Table 3: Sample important Classes (prefix YRI_CPP_ to class name) & Methods of C++ Library ”YRI_SD_RUNTIME_VERIF”. N◦CLASSES METHODS UTILITY 1. MONITOR CREATE_MONITOR Creates a new runtime monitor 2. MONITOR YRI_register_set_final_state_CALLBACK_FUNCTION register a C++ method a the callback function in case an error state was found. 3. MONITOR RESET_RUNTIME_MONITOR Sets the current state TO the start state. 4. MONITOR YRI_trigger_an_edge_event "TRUE" is returned in case an edge event "an_edge_event" was triggered. 5. MONITOR create_yri_monitor_state Creates a runtime monitor state. 6. MONITOR create_yri_monitor_edge Creates a runtime monitor edge. 7. MONITOR find_yri_monitor_state Search for a runtime monitor state within a runtime monitor. 8. MONITOR set_RUNTIME_MONITOR_NAME Sets an identity name to a runtime monitor. 9. MONITOR IS_in_TRACE_LOG 10. MONITOR TRACE_LOG_current_RECEIVED_EVENT_TOKEN 11. MONITOR GET_root_edge 12. MONITOR DELETE_yri_monitor_edge 13. notinset_inset_TRACE_expression YRI_CPP_notinset_inset_TRACE_expression 14. notinset_inset_TRACE_expression set__USE_SQL_SYNTAX_event_logging__FOR_PRINTING We place and explain sample methods of C++ Library ”YRI_SD_RUNTIME_VERIF” that WE deem of major interest for developers : 1.) 4.1 Generated Method YOU need to code Author: Xavier Noundou [Pr. Prof. Dr.–Ing. ] Holy-Ghost. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "12 / 16". | Version of – October 15, 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 – October 15, 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. [CHKS12] Franck Cassez, Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors. Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28-30 November 2012, volume 102 of EPTCS, 2012. [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/17362697, 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 – October 15, 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 – October 15, 2025 – YERITH_QVGE user’s guide 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 9.“) ..... 4 2 YERITH_QVGE Design and Testing System Dependencies .......................................... 7 3YRI-DB-RUNTIME-VERIF Directories ......................................................... 8 Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "3 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide 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 9.“) 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 Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "4 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide YERITHr&d Figure 5: SAMPLE INTERNET-RELATED USE CASE SCENARIO OF "SDMM ". Internet WWW / (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 parallel process management runtime execution and thread resources. implement YRI−DB−RUNTIME−VERIF A PCI−CARD could also 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 } Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "5 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide YERITHr&d Figure 6: A SCREENSHOT OF YERITH_QVGE. Figure 7: A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL EVENT LOG. 1 Introduction Figure 8: SOFTWARE ARCHITECTURE OF YRI-DB-RUNTIME-VERIF. OPERATING SYSTEM (OS) MYSQL library methods calls OS system calls yri−db−runtime−verif QT socket calls (via Qt−Dbus) A RUNTIME MONITOR LIBRARY − PLUGIN PUA / SUT (JVM−java virtual machine) PUA source code instrumented This user’s guide helps briefly and concisely how to create a binary executable of the runtime monitoring testing tool YRIDB-RUNTIME-VERIF having user defined runtime monitors. The guide also specifies keywords allowed within runtime monitor specifications as State Diagram Mealy Machines. YERITH_QVGE (YRI_QVGE) could be used for the following automatic generation, analysis, verification, and validation tasks: 1. Automatic generation of runtime monitoring module program to prove whether a test procedure, automated, or not, is correct with regards to a test and / or design STATE DIAGRAM MEALY MACHINE (formally described in [Nou23]). In effect, let the test execution be runtime monitored to watch whether accepting error states would be found. For instance, Junit testing environment could automatically integrate an automatically generated runtime monitor infrastructure for unit testing. 2. Automatic generation of runtime monitoring module program for any software that can emit DBus messages. ”Such runtime monitoring modules are for interest for special LTL model checking properties that cannot get a definite answer through use of a conventional model checker”. 3. Software design properties with SQL 4. Software design properties including event sequences over different layers of software system architecture 5. Class diagram with sequence diagram. 1https://www.github.com/yerithrd/yri_sd_runtime_verif 2https://www.github.com/yerithrd/yri-db-runtime-verif Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "6 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide YERITHr&d 2 YERITH_QVGE (YRI_QVGE) Short Overview Figure 9: YERITH_QVGE software library dependencies. YRI_SD_RUNTIME_VERIF_LANG YRI_SD_RUNTIME_VERIF_LANG_COMP YRI_SD_RUNTIME_VERIF_UNIT_TESTS Runtime monitor container (e.g.: YRI−DB−RUNTIME−VERIF) Design SDMM; from CASE tool (e.g.: YERITH_QVGE) YERITH_QVGE is a CASE (Computer-Aided Software Engineering) design tool to generate "domain-specific language (DSL) YRI_SD_RUNTIME_VERIF_LANG 1" files, to be inputted into the "compiler YRI_SD_RUNTIME_VERIF_LANG_COMP", so to generate C++ files for the "runtime verifier tester YRIDB-RUNTIME-VERIF 2" that allows for manual verification of SQL correctness properties of Graphical User Interface (GUI) software. Figure 10 illustrates a workflow diagrammatically of the afore described process. Figure 9show a diagram of the afore described process; The step of the unit tests is colored in gray because it is only for developers of YERITH_QVGE intended. YRI-DB-RUNTIME-VERIF inputs SQL correctness properties expressed using the formalism "state diagram mealy machine (YRI_SD_RUNTIME_VERIF_LANG)". Figure 8illustrates a software system architecture of YRI-DB-RUNTIME-VERIF, together with the monitored program under analysis. The Free Open Source Code Software (FOSS) tool-chain of development testing is located as follows for free, EXCEPT for "YERITH_QVGE " that is a Closed Source Code Software (CSCS): •COMPILER (i.e.: YRI_SD_RUNTIME_VERIF_LANG_COMP): https://www.github.com/yerithrd/yri_sd_ runtime_verif_lang •RUNTIME VERIFIER TESTER (i.e.: YRI-DB-RUNTIME-VERIF): https://www.github.com/yerithrd/ yri-db-runtime-verif •state diagram mealy machine UNIT TESTS CODE (i.e.: YRI_SD_RUNTIME_VERIF_UNIT_TESTS): https://www.github.com/yerithrd/yri_sd_ runtime_verif_UNIT_TESTS •state diagram mealy machine (i.e.: YRI_SD_RUNTIME_VERIF_LANG): https://www.github.com/yerithrd/yri_sd_ runtime_verif 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: •Theprogramis in a start state D; state Disastartstatesince 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. Thisshallnot be thecasesince department ’YRI_ASSET’ isnomoredefinedinSUT database table ’department’. 3Scientific: fail (forbidden) trace. 4Structure Query Language. Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "7 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide YERITHr&d 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: 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". Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "8 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide YERITHr&d 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 incase auser don’tspecify aSQL commandquery, since it could be leaved empty: Subsections 9.1.1,9.1.2,9.1.3, and 9.1.4 describe the strategy implemented. 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 in_after (DD,YR)ACTION (RECOVERY_D) in_after (YX,YY) 9.1.4 Concrete RECOVERY 2 action (Practical solution to be implemented in YRI-DB-RUNTIME-VERIF. 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. Author: Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing. ] Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "9 / 11". | Version of – October 12, 2025 – YERITH_QVGE user’s guide YERITHr&d 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 "10 / 11". | Version of – October 12, 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 "11 / 11". | Version of – October 12, 2025 – YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 List of Tables 1.1 COMPARISON TABLE BETWEEN C++ [Ste90], Javascript [Fla20], AND JAVA [AGH00]. Javascript and JAVA only have virtual machines that are in FACT REACTIVE SYSTEMS ! .12 1.2 YERITH–ERP–9.0 RELEVANT SOFTWARE SYSTEM METRICS .................. 14 2.1 Thick client application VS Webbrowser based application (with solutions of YERITHr&d now (2025)). ........................................... 18 3.1 Thick client application VS Webbrowser based application. . . . . . . . . . . . . . . . . . . . . 19 6.1 Yerith–Erp–9.0–PLATINUM (Yerith–Erp–Pgi–9.0–Web–System) VS. Odoo.............. 25 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 7 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 8 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 List of Listings 5.1 A sample very limited for explanation & illustration purpose yerith–web–dsl–9.0 Source code ! 24 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 9 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 10 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Chapter 1 Introduction This introduction motivates why I created Yerith–Erp–9.0, and why it uses the best software programming language AND METHODOLOGY (OOP: OBJECT–ORIENTED PROGRAMMING) of its time ! 1.1 Motivation Figure 1.1: BUSINESS workflow of ERP software Yerith–Erp–9.0 customers, suppliers, and / or BUSINESS data about clients Employees are manipulated. mandotory connections. Blue colored arrows are not Red colored arrows are mandotory connection for a well funtioning YERITH−Erp−9.0 System. Generated Static / DYNAMIC web sites customers and / or clients a computer network to deliver Maximum performance to their Employers All yerith−erp−pgi−platiNum computers colaborate throughout YERITH−ERP−PGI−9.0−platiNum Yerith R&D Yerith−erp−pgi platiNum COMPONENTS Workflow Business Information / Data Report Runtime Monitoring Verification YRI_QVGE: are checked by this component alerts about stocks, etc. Human REsource (HR) payments, System−daemon : Barcode Scanner Web−SYSTEM Configurations−data User of Yerith−Erp−Pgi−9.0−PlatiNUM DBMS BASE Data Size − Large / Medium / Small Large / Medium / Small Dining Room − Yes / No Bedroom #1 Price: Linen Closet Distinguishing Features: Address: Plumbing − New / Old Bathrooms: 1 1+ 2 Tub / Shower Termite Report: Yes / No $ Bedrooms: 2 2+ 3 Closets − Large / Medium / Small Living Room Large / Medium / Small Fireplace Laundry Yes / No Heating System Floor / Wall / Central Roof − New / Old Other Wiring − New / Old 110V / 220V Windows − Casement / Double Hung / Other: Stove − Gas / Electric Cabinets − Many / Few New / Old Pantry Sink − Large / Small Porcelain / Stainless Kitchen Outside Garage − One car / Two car Yard Large / Medium / Small Bedroom #2 Size − Large / Medium / Small Closets − Large / Medium / Small Sink − Large / Small Porcelain / Stainless Wiring − New / Old 110V / 220V Distinguishing Features: Heating System Windows − Casement / Double Hung / Other: Size − Large / Medium / Small Living Room Yerith–Erp–9.0 [NOU22,NOU21a,NOU21b] is an Enterprise Resource Planing (ERP) software system that aims ’effectiveness’ and ’simplicity’, compared to other high ranked ERP software systems (e.g.: ’Sage Gescom i7’, ’SAP Business One’, ’Odoo’, etc.). Yerith–Erp–9.0 is implemented by me with THE USER INTERFACE LIBRARY QT [Ltd22]. Our goal when designing and implementing this ERP software system is morefolds: 1) RENDER ENTERPRISE RESOURCE PLANING (ERP) SOFTWARE SYSTEM USAGE AND MANIPULATION AS EASY AS READING A LEISURE OR RECREATIONAL BOOK SO TO REDUCE USER STRAIN SIZE ! 2) CONTRIBUTE TO REDUCE POVERTY BY IMPROVING SOFTWARE SYSTEM TECHNOLOGY FOR ENTERPRISE RESOURCE PLANING (ERP). Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 11 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 1.1.1 Application Domain Yerith–Erp–9.0 can be used by any managerial organization, WHETHER governmental, OR NON GOVERNMENTAL (N.G.O) ! Yerith–Erp–9.0 is aimed at being simpler in usage and manipulation than older top ranked ERP software systems (e.g.: ’Sage Gescom i7’, ’SAP Business One’, Odoo, etc.) ! A DETAILED COMPARISON OF OCCURS IN PAPER [NOU21a]! Applications domains of Yerith–Erp–9.0 are for instance: 1. engineering offices; 2. insurance companies; 3. attorney offices; 4. etc. 1.1.2 Implementation Technology Table 1.1: COMPARISON TABLE BETWEEN C++ [Ste90], Javascript [Fla20], AND JAVA [AGH00]. Javascript and JAVA only have virtual machines that are in FACT REACTIVE SYSTEMS ! FEATURES C++ Javascript Java 1. PROGRAMMING LANGUAGE PHILOSOPHY object–oriented object–oriented object–oriented 2. MACROS Ø Ø 3. MULTIPLE INHERITANCE Ø 4. support INTERFACES Ø Ø Ø 5. STATIC COMPILATION Ø 6. RUNTIME MONITORING & VERIFICATION Ø(YRI_DB_RUNTIME_VERIF)Ø Ø 7. UNIT TESTING FRAMEWORK Ø Ø Ø 8. NETWORK CAPABLE Ø Ø Ø 9. CROSS PLATFORM PORTABLE Ø Ø Ø 10. include FILE LIBRARY CAPABILITY Ø 11. MULTI THREADING Ø Ø 12. WYSIWYG GUI DESIGN TOOL Ø Ø 13. VIRTUAL MACHINE IS A REACTIVE SYSTEM Ø Ø We found following reasons for introduction of virtual machines in the programming languages Javascript, and JAVA: •JAVA and Javascript overcome runtime monitoring requirements by introducing language interpretation via virtual machine implementation and execution of programs. •C++ doesn’t have a mainstream equivalent to date; due to its compiled nature. I advocate YRI_DB_RUNTIME_VERIF as the component through which any programming language may have for free by runtime execution, runtime monitoring capability. We chose to design and implement Yerith–Erp–9.0 as a thick client software system because of the following reasons: 1. The implementation language C++ offers much flexibility: Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 12 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 1. MULTIPLE INHERITANCE: It allows developers to abstract as much as possible business code upwards, away from downwards implementation classes. For instance, in Yerith–Erp–9.0, GUI Qt windows inherits for instance search filtering feature, and print capability from 2different classes. Print capability couldn’t be inherited from the same class where search filtering is abstracted and partially implemented (interface in JAVA for instance doesn’t allow any method body code), because it works in its pure abstract class (C++ class with at least 1empty method body), together with feature database column filtering for viewing and printing. The drawback of the multiple inheritance in C++ is: it sometimes can be very difficult to build it using "gcc (g++)[GCC]" ! 2. MACROS: They enable developers to create TEXT TEMPLATE in their code. For instance, I use macros in some parts of my code to reduce execution time and stack activation records size for method or function calls in Yerith–Erp–9.0 ! 2. The availability of ’WHAT YOU SEE IS WHAT YOU GET’ (WYSIWYG) tools for fast and useful user interface design (e.g.: Qt designer [Com20], miniStudio (vxWorks) [WEI20], etc.) 3. The low number of logical software system architecture layer (i.e.: 2.) involved with the use of a thick client software system architecture, as opposed to a webbrowser based software system (i.e.: 4,client user interface,presentation layer,business logic, and data (DBMS)). FURTHERMORE, TABLE 1.1 ILLUSTRATES A FEATURE COMPARISON TABLE BETWEEN object oriented languages C++,Javascript, and JAVA! Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 13 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 1.1.3 Software System Current Metrics Table 1.2: Yerith–Erp–9.0 RELEVANT SOFTWARE SYSTEM METRICS Software System Metric Value User Interface (windows, dialog) number 60 MariaDB SQL table number 40 MariaDB SQL table column number 320 Latex template for PDF printing 75 Source lines of code (SLOC) 390, 000 1.2 Overview This pamphlet is structured as follows: 1. Chapter 1motivates why I created Yerith–Erp–9.0, and why it uses the best software programming language AND METHODOLOGY (OOP: OBJECT–ORIENTED PROGRAMMING) of its time ! 2. Chapter 2tabular evaluates why thick client are BETTER THAN webbrowser based software system architectures ! 3. Chapter 3explains why Yerith–Erp–9.0 is modular in its uses, and fits any industrial setting. 4. Chapter 5introduces Yerith–Erp–Pgi–9.0–Web–System (https://github.com/yerithrd/ yeritherppgiwebsystem)that encompasses 2projects to deliver for free, Without much computer programming webshops for Yerith–Erp–9.0 clients and / or customers : A.Yerith–Web–Pages–Generator–9.0 : this project delivers webshop programming using a new simple Domain–Specific Language (DSL) with a compiler / translator that generates automatically PHP source code for its users. https://github.com/yerithrd/yerith-web-pages-generator-9 B.Yerith–Web–Design–Tool : This QT–trolltech additional tool that enables webshop automatic source code generation based on user drawn widgets using Qt designer. https://github.com/yerithrd/yerith-erp-9-0 C.ALL functionalities will be available only on USB–dongle key on shopping stores as commercial priced product. 5. Chapter 6explains why Yerith–Erp–9.0 uses the BEST SOFTWARE TECHNOLOGY IN TERMS OF SOFTWARE SYSTEM ARCHITECTURE ! Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 14 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Chapter 2 Thick Client VS. Webbrowser based Software System Architecture This comparison chapter tabular evaluates why thick client are BETTER THAN webbrowser based software system architectures ! 2.1 Thick client: 2layers logical software architecture Figure 2.1: 2layers logical architecture of thick client software system (Image copied from [sec20]). A thick client software architecture may also have more than only 2layers. 2.1.1 Security Leak We advocate to create a runtime verification monitoring tool that protect de-compilation and / or reverse engineering of code source and / or binaries within a productive environment !!! Program Code–binary obfuscation could also be an alternative solution to avoid de-compilation and / or reverse engineering in order to destroy !!! 1. A copy of a commercial software on your local hard drive is an enormous amount of money that was invested into your local computer, With a risk for a company that you crack–dishonest their cryptographic protection design to secure their source / binaries code on your hard drive !!! IN EFFECT, de-compiling your binary software code is not possible at all !!! IN EFFECT, a commercial onerous software binaries shall be sold only installed into a USB–dongle key, Since only its user can have access to it. 2. With a web–browser based software architecture, not anyone could know which software you are using because none is installed on your hard drive; THIS could be for instance advantageous for banking software for instance as no one except its user could know how to access it from a local computer web– browser !!! Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 15 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 2.2 Webbrowser based: at least 4layers logical software architecture Figure 2.2: Webbrowser–based software architecture : at least 4layers logical software architecture (Image modified from online pdf paper "FlashCache: A NAND Flash Memory File Cache for Low Power Web Servers" [ https://doi.org/10.1145/1176760.1176774] by Trevor et al..). YRI–DB–RUNTIME–VERIF runtime monitors communication layers. Yr−Db−Runtime−Verif analyzes & verifies communications bewteen layers YRI−QVGE−PC−Tablet QT−Designer tool as What You See Is What You Get design Tool (WYSIWYG Tool) 2.2.1 Software Vulnerability 1. 1intrusion of a malware–software into an application server; Example like ”IBM–Websphere”; ”Apache Tomcat”; etc.; Causes a malfunction of a store–organization network completely. ÆSuch software vulnerabilities don’t exist with thick client software system ! 2.2.2 NETWORK connection related issues & problems 1. The probability to have malfunction of your software system is high because of the network probable deficiency due to at least 3layers of inter–connection between your local tier–view (Tiers –1as depicted in Figure 2.2); and your remote Application And / Or Database server !!! 2.2.3 BUSINESS related data & INFORMATION Issues with Web–Browser based Architecture Software Systems A.) Since all or part of your business data critical are only located on a hard–drive outside of your local area network (LAN), There might be issues with following legal & documentary aspects : 1. Disruption of WAN (Wide Area Network) and / or Internet might prevent you indefinitely to access your business data. 2. LAWS of the country–place where you locate your data might endanger your business; Partly because it is different from your local laws where you officially have registered your business venture ! ON the other hand side of it; Remote location of your business data in a better country–place might favor your business compared to where it is locally registered ! It might be allowed in that remote country–place to perform certain digital ideas and things that are forbidden where your original business is located : for instance PORNOGRAPHY, etc. ! You may expose yourself to legal prosecutions in the latter case; Either in the remote country– place of your remote digital activities–server, Or locally where this digital activity is Prohibited– by–laws !!! Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 16 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Chapter 5 Yerith–Web–Pages–Generator– 9.0 : Website Application FOR free THIS chapter introduces a software–system that we started invention and / or creation this current year 2024, As an alternative solution for our clients. Users of Yerith–Erp–9.0 could then with Yerith–Web–Dsl– 9.0 automatically generate website applications for their goods and services to share with clients and / or other people abroad ! 5.1 What You See Is What You Get (WYSIWYG-Tool) : Yerith–Web–Design–Tool Figure 5.1: A SOFTWARE architecture overview of Yerith–Web–Pages–Generator–9.0 ("An SDMM usage scenario by IBM– websphere".) Figure 5.2: Yerith–Web–Pages–Generator–9.0 generates legacy web files from Qt 5interface files (”.ui” files). Flex, Bison Yerith−web−pages−generator−9.0−DSL Translator Optional Step HTML / CSS / PHP / Javascript, etc. generated files Application Server Running Oracle−open−JAVA−jdk Script files (.spec_html) Yerith−web−pages−generator−9.0−DSL QT−ui (.ui) user interface files Yerith−Web−Design−Tool (WYSIWYG C++ tool) YRI−DB−RUNTIME−VERIF runtime monitoring verification Figure 5.3: A Stack Stapled Architecture Overview of Yerith–Web–Pages–Generator–9.0. Cyber−Security SDMM (E.g.: taint−analysis) (E.g.: No−write−After−Close) Runtime memory SDMM Optimizating−compiler Other User−specific SDMM drawing−design SDMM PHP − Java QUERCUS Application Server Quercus Application Server Running on Oracle−open−jdk PHP Code from YERITH−WEB−DSL−9.0 Dbus emit messages Dbus emit messages YRI−DB−RUNTIME−VERIF Runtime Monitoring Service Common non–technical users of Yerith–Erp–9.0 cannot program a website. To encourage such users to create their webshops using Yerith–Erp–9.0; We introduce ”Yerith–Web–Dsl–9.0”, And ”Yerith–Web–Design–Tool” : 1.)Any stock inventory and stock service introduced within Yerith–Erp–9.0 could then be converted into a web presentation shop using both technologies; ”Yerith–Web–Dsl–9.0” is a high–level view programming language to create web HTML5–PHP pages by describing them more simply than using raw conventional, since year 1990,HTML5(and PHP) programming web languages. Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 23 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Listing 5.1: Asampleverylimitedforexplanation&illustrationpurpose yerith–web–dsl–9.0 Sourcecode! 1 yerith−web−pages−generator−MAIN YECEFOIQ−WEB−PAGES 2 { 3 4 web−html−page yri_test 5 { 6# ’C’omments. # 7 yri_html_page_title: ’Bienvenue !’; 8 yri_html_page_MENU_BAR_link_string: ’yri_test !’; 9 yri_html_page_input_header_menu_bar[web−html−page−menu−bar−headers]; 10 }; 11 12 13 web−html−page index 14 { 15 yri_html_page_title: ’Bienvenue au centre de formation qualifiante Yecefoiq !’; 16 17 yri_html_page_MENU_BAR_link_string: ’yri_index !’; 18 19 yri_html_page_input_header_menu_bar[web−html−page−menu−bar−headers]; 20 21 yri_html_page_text_SECTION (HTML_HEADER_H/3; ’Description du Centre de Formation’) 22 { 23 VARIABLE_YRI_PARAGRAPH variable_paragraph_1 24 {text−yri−font−size = 11} : 25 {text−yri−width−box = 5 cm} === 26 "Ce centre de formation en Informatique est la proprit de 27 la start−−up entrepreneuriale de Gnie des Systmes de 28 Gestion Informatiss YERITH RD. 29 Les cours du centre de formation ont pour cibles les 30 personnes suivantes:" 31 32 li_begin: ’Travailleurs qualifis en Informatique.’ 33 li: ’Travailleurs qualifis en Sciences et en Gnie.’ 34 li: ’lves et coliers des tablissements confessionnelles vangliques.’ 35 li: ’tudiants dans les universits publiques confessionnelles vangliques.’ 36 li_end: ’tudiants dans les universits du monde moderne 37 (incluant des catholiques orthodoxes).’ 38 }; 39 }; 40 41 web−html−page−menu−bar−headers 42 { 43 # vertical−left vertical−right horizontal−top # 44 web−html−page−menu−bar−headers_Position = ’vertical−left’; 45 46 yri_html_page_section[index, 47 yri_test, 48 a_propos, 49 programme_des_cours, 50 contenu_des_cours, 51 impressum]; 52 }; 53 } Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 24 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Chapter 6 Conclusion This conclusion explains why Yerith–Erp–9.0 uses the BEST SOFTWARE TECHNOLOGY IN TERMS OF SOFTWARE SYSTEM ARCHITECTURE ! Table 6.1: Yerith–Erp–9.0–PLATINUM (Yerith–Erp–Pgi–9.0–Web–System) VS. Odoo. Artifacts Yerith–Erp–9.0–PLATINUM Odoo libraries & programs YERITH_QVGE, etc. pythonlxml, etc. user interface code TOOLS WYSIWYG QT–DESIGNER (CUSTOM BUILD) FRAMEWORKS business code PHP (partly generated), C++ Python,JavaScript Database Management Server (DBMS) MySQL PostgreSQL web server Quercus Werkzeug Yerith–Erp–9.0 has a thick client software system architecture because we found thick client software system architectures simpler than webbrowser based software system architectures. Thick client software system architectures is simpler because it requires less layers in its logical (or physical) software system architecture, and is easier to develop and maintain as a software system application. Table 2.1 illustrates a thick client software system is SUPERIOR IN TERMS OF TOOLS FOR MAINTENANCE AND DEVELOPMENT than a webbrowser based software system ! A webbrowser based software system architecture has more drawbacks as follows: 1.)it requires at least 2other software systems, apart from the ones normally required by developed software system itself, for instance libraries (e.g.: Log4j), to fully operate (e.g.: web server, application server, etc.). Table 6.1 depicts this situation in the light of the open source ERP software system Odoo. Accordingly, a thick client software system doesn’t require any running and managing infrastructure such as for example an application server ! 2.)A webbrowser based software system requires at least 4layers in its logical system architecture (e.g.: client, presentation, logic, and data layers). Accordingly, a thick client software system only requires at least 2layers ! 3.)A webbrowser based software system potentially entails more software security vulnerabilities because its implementation requires the use of at least 2different programming languages, and frameworks in combination. Accordingly, a thick client software system needs only the use of 1homogeneous software programming language ! Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 25 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 26 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Chapter 7 Bibliography [AGH00] Ken Arnold, James Gosling, and David Holmes. The Java Programming Language. Addison Wesley Longman Publishing Co., Inc., USA, 3rd edition, 2000. [Com20] The Qt Company. Qt Designer Manual. https://doc.qt.io/qt-5/qtdesigner-manual. html, 2020. Last accessed on September 4,2020 at 15:21. [DEB22] DEBIAN. Debian – The Universal Operating System. https://www.debian.org, 2022. ACCESSED LAST TIME on JUNE 12,2022 at 12:10. [Fla20] David Flanagan. JavaScript: The Definitive Guide: Master the World’s Most-Used Programming Language 7th Edition. O’Reilly, 2020. [GCC] THE COMPILER SUITE GCC. THE GCC (G++) COMPILER SUITE. https://www..org/. Last accessed on December 29,2020 at 12:00. [Ltd22] The Qt Company Ltd. Qt is a C++ toolkit for cross-platform application development. https: //www.qt.io, 2022. ACCESSED LAST TIME on JUNE 12,2022 at 18:00. [Mar22] MariaDB.org. MariaDB Foundation - MariaDB.org. https://www.mariadb.org, 2022. ACCESSED LAST TIME on JUNE 24,2022 at 12:20. [NOU21a] XAVIER NOUNDOU. GROUPED PRESENTATIONS DOCUMENTS OF YERITH–PGI– 3.0. https://archive.org/download/yerith-erp-9-0-info-english_202104/ yerith-erp-9-0-info-english.pdf, 2021. ACCESSED LAST TIME ON june 17,2022 at 08:40. [NOU21b] XAVIER NOUNDOU. INSTALLATION GUIDE FOR ERP SOFTWARE SYSTEM YERITH–ERP–9.0. https://archive. org/download/yerith-erp-9-0-installation-guide-standalone/ yerith-erp-9-0-installation-guide-standalone.pdf, 2021. ACCESSED LAST TIME ON june 17,2022 at 08:20. [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, 2022. ACCESSED LAST TIME ON June 22,2022 at 12:00. [sec20] securityboulevard.com. Thick Client Penetration Testing Methodology. https:// securityboulevard.com/2020/02/thick-client-penetration-testing-methodology/, 2020. Last accessed on September 4,2020 at 15:21. [Ste90] W. Richard Stevens. UNIX Network Programming. Prentice-Hall, Inc., USA, 1990. [WEI20] Yongming WEI. miniStudio User’s Guide. https://www.minigui.net/en/ministudio, 2020. Last accessed on September 4,2020 at 15:21. Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 27 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 28 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Index 1–page presentation of Yerith–Erp–9.0,28 2layers logical architecture of thick client software system, 15 2–pages presentation of Yerith–Erp–9.0,33 4layers logical architecture of webbrowser based software system, 16 Yerith–Erp–9.0 VS. Odoo webbrowser based software system, 25 comparison of Yerith–Erp–9.0 against others, 29 comparison table between thick client and webbrowser based software system, 18 motivation for creating Yerith–Erp–9.0,11 point of sale proposed hardware, 30 Sample 2–computers store, 20 sample decentralized multi sites supermarket, 20 STRUCTURE OF THIS PAPER, 14 Webbrowser based: now 2layers with QT– trolltech-WebAssembly & YERITHr&dYerith-Web-Dsl-9.0, 17 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 29 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 30 OF 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 Appendix A Presentation Documents of open source software system YERITH–ERP–9.0 Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 31 DE 37 VERSION OF October 12, 2025 YERITHr&d WWW - World Wide Web (WWW) Design & Programming using yerith–web–dsl–9.0 YERITHr&d |YERITH–ERP–9.0 software system product sheet YERITH–ERP–9.0 Software System Product Sheet YERITH–ERP–9.0 is an ERP software system with 6user roles, and types: 1. « Administrator » 2. « Business manager » 3. « Cashier » 4. « Seller » 5. « ASSET – stock manager » 6. « Storekeeper ». YERITH–ERP–9.0 features: 1. Runtime monitoring verification with ”yerith_qvge (https: //github.com/yerithrd/yri-db-runtime-verif) ”; 2. alerts over stock quantity, and, time period; 3. BA–Business Analytics (business dashboard); 4. HR (human resources) — ALSO with automated and / or manual payment handling for employees; customer relationship management (CRM), budget line management; 5. sale management (e.g. point of sale); 6. ASSET – stock management (e.g. check in); 7. user, and role administration; 8. wild-char searches with character %. YERITH–ERP–9.0 is: 1. easier, and, intuitive, in its use 2. lighter, and, faster, in memory usage 3. multi sites. YERITH–ERP–9.0’s runtime memory usage test is realized using run–time software analysis tool valgrind. GENERAL SOURCE CODE QUALITY CONTROL is realized with compile–time code analysis tool Cppcheck. Business manager’s main window BUSINESS workflow of YERITH– ERP–9.0 Yerith−erp−pgi platiNum business Workflow Employees are manipulated. customers, suppliers, and / or BUSINESS data about clients All yerith−erp−pgi−9.0−platiNum customers and / or clients computers collaborate throughout a computer network to deliver Maximum performance to their Employers. YERITH−ERP−PGI−9.0−platiNum Business Report Information / Data ThermaL−Printer Epson−TMT20ii Barcode scanner Yerith R&D High Disk Speed Sink − Large / Small Porcelain / Stainless Wiring − New / Old 110V / 220V Distinguishing Features: Heating System Windows − Casement / Double Hung / Other: Size − Large / Medium / Small Living Room Sink − Large / Small Porcelain / Stainless Wiring − New / Old 110V / 220V Distinguishing Features: Heating System Windows − Casement / Double Hung / Other: Size − Large / Medium / Small Living Room OPERATIONS Point of Sale Hardware ØBarcode scanner ØThermal printer, etc. Database Management Systems Ømariadb 10.5. Operating Systems ØDebian–Linux 11; 12. Author: ”Xavier Noumbissi Noundou [Pr. Prof. Dr.–Ing.]” Version of – October 12, 2025 – Esprit–Saint. YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) 32 OF 37 VERSION OF October 12, 2025 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) 2 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) Table des matières Table des matières 3 Table des figures 5 Liste des tableaux 7 1 INTRODUCTION 9 1.1 Définitions ......................................... 9 1.1.1 Filiale (DICTIONNAIRE ROBERT)..................... 9 1.1.2 Succursale (DICTIONNAIRE ROBERT).................. 9 2 Configuration D’1ORDINATEUR D’1SUCCURSALE 11 2.1 INSTALLATIONS DE yerith–erp–pgi–9.0 PAR SUCCURSALE . . . . . . . . 12 3 CAS D’1Filiale 13 3.1 TPE et PME ........................................ 13 3.2 Très Grandes Entreprises (TGE) ........................... 14 4 CAS D’1Succursale 15 4.1 Coupure de connexion Internet ............................ 16 5 LOGIN et connexion à 1succursale 17 6 Bibliographie 19 3 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) 4 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) Table des figures 1 WORKFLOW de travail générique de YERITH–PGI–9.0............ 1 2.1 FIGURE ILLUSTRATIVE de la marque succursale ................ 11 3.1 BASE DE DONNÉES CENTRALISÉE d’1filiale POUR TPE / PME ...... 13 3.2 BASE DE DONNÉES CENTRALISÉE d’1filiale pour TGE ........... 14 4.1 BASE DE DONNÉES décentralisée du SIÈGE CENTRAL ............ 15 5.1 Connexion à 1succursale (SOCIÉTÉ – SITE) ................... 17 5 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) 6 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) Liste des tableaux 7 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) 8 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) Chapitre 1 INTRODUCTION LE PROGICIEL DE GESTION INTÉGRÉ YERITH–PGI–9.0 [uNu22,uNu23a,uNu23b] permet à ses utilisateurs la réutilisation de la fonctionnalité "multi-sites (succursales)"! La fonctionnalité "multi-sites (succursales)" permet à 1organisation de contrôler ses activités décentralisées de façon centralisée à l’aide de YERITH–PGI–9.0. Les opérations des succursales (ou encore d’1filiale) sont répertoriées dans la base de données (MySQL) à l’aide de la colonne ’localisation’. ’Lacolonnelocalisation’ de la base de données "yerith_erp_9"CORRESPOND À : 1. Localisation (INSTALLATION EN FRANÇAIS) 2. Site (EN ANGLAIS) dans les interfaces graphiques (GUI) de YERITH–PGI–ERP–9.0. 1.1 Définitions 1.1.1 Filiale (DICTIONNAIRE ROBERT) Société jouissant d’une personnalité juridique (à la différence de la succursale) mais dirigée ou contrôlée par une société mère. 1.1.2 Succursale (DICTIONNAIRE ROBERT) Établissement qui dépend d’un siège central, tout en jouissant d’une certaine autonomie. Exemple : Les succursales d’une banque. 9 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) 10 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) Chapitre 2 Configuration D’1ORDINATEUR D’1 SUCCURSALE Figure 2.1 – FIGURE ILLUSTRATIVE de la marque succursale CHAQUE ORDINATEUR INSTALLÉ DANS 1SUCCURSALE possède 1identification égale à 1CHAÎNE DE CARACTÈRE unique. CETTE CHAÎNE de caractère est la même pour chaque ordinateur de la succursale observée. LA FIGURE 2.1 illustre L’IDENTIFIANT "YERITH_RD_TEST" d’1succursale de test. Il s’agit de L’ONGLET "Connecter une localisation" dans la fenêtre ’FENÊTRE DE L’ADMINISTRATEUR’! 11 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) 18 DE 19 YERITHr&d YERITH–ERP–PGI–9.0: Configuration MULTI–SITES (SUCCURSALES) Chapitre 6 Bibliographie [uNu22] XAVIER NOUMBISSI NOUNDOU. YERITH–ERP–PGI–9.0 DOCTORAT COMPENDIUM. https://archive.org/download/ yerith-erp-pgi-compendium_202206/JH_NISSI_ERP_PGI_COMPENDIUM. pdf, 2022. ACCÉDER POUR LA DERNIÈRE FOIS le 29 Mars 2023 à09:00. [uNu23a] XAVIER NOUMBISSI NOUNDOU. GUIDE D’INSTALLATION POUR LE PROGICIEL DE GESTION INTÉGRÉ YERITH–PGI–9.0. https://archive. org/download/yerith-erp-9-0-guide-dinstallation-standalone_ 202303/yerith-erp-9-0-guide-dinstallation-standalone.pdf, 2023. ACCÉDER POUR LA DERNIÈRE FOIS le 29 mars 2023 à12:00. [uNu23b] XAVIER NOUMBISSI NOUNDOU. INSTALLATION GUIDE FOR ERP SOFTWARE SYSTEM YERITH–ERP–9.0. https://archive.org/ download/yerith-erp-9-0-installation-guide-standalone_202304/ yerith-erp-9-0-installation-guide-standalone.pdf, 2023. ACCESSED LAST TIME ON APRIL 18,2023 at 08:05. 19 DE 19 YERITH_QVGE : A Framework for Verifying SQL Correctness Temporal Properties of [GUI] Software at Runtime Xavier noumbissi Noundou1 1Yaounde, Center region, Cameroon. Contributing authors: yerith.xa[email protected]; Abstract Software correctness properties are essential to maintain quality by continuous and regressive integration testing, as well as runtime monitoring the program after customer deployment. This paper presents an effective and lightweight C++ program verification framework: YRIDBRUNTIMEVERIF, to check SQL (Structure Query Language) [1] software correctness properties specified as temporal safety properties [2]. A temporal safety property specifies what behavior shall not occur, in a software, as sequence of program events. YRIDBRUNTIMEVERIF allows specification of a SQL temporal safety property by means of a state diagram mealy machine [3]. In YRIDBRUNTIMEVERIF, a specification characterizes effects of program events (via SQL statements) on database table columns by means of set interface operations (∈, /∈), and, enable to check these characteristics hold or not at runtime. Integration testing is achieved for instance by expressing a state diagram that encompasses both Graphical User Interface (GUI) states and MySQL [4] databases queries that glue them. For example, a simple specification would encompass states between ’Department administration’ and ’Stock listing’ GUI interfaces, and transitions between them by means of MySQL databases operations. YRIDBRUNTIMEVERIF doesn’t generate false warnings; YRIDBRUNTIMEVERIF specifications are not desirable (forbidden) specifications (fail traces). This paper focuses its examples on MySQL database specifications, labeled as states diagrams events, for the newly developed and FOSS (Free and Open Source Software) Enterprise Resource Planing Software YERITH–ERP–3.0 [5]. Keywords: model-based testing, reactive system analysis, computer software program analysis, computer software dynamic program analysis, software integration testing with SQL and GUI, runtime monitoring 1 Fig. 1:YRIDBRUNTIMEVERIF WORKFLOW (diagram inspired from operation diagram in [6]). Ongoing report program state on erroneous SUT and lines of code yri_sd_runtime_verif_lang STATE DIAGRAM SPECIFICATIONS as DSL code as yri_sd_runtime_verif STATE DIAGRAM SPECIFICATIONS C++ code DYNAMIC RUNTIME ANALYSIS (SUT + yri−db−runtime−verif) as separate processes SUT + yri−db−runtime−verif run conccurrently SUT emits SQL events to yri−db−runtime−verif PROGRAMS OUTPUT corelation SUT receives user GUI events that modify SQL database tables yri−db−runtime−verif monitors and analyzes SUT SQL event sequence 1 Introduction Table 1:YERITH–ERP–3.0 RELEVANT SOFTWARE SYSTEM METRICS Software System Metric Value User Interface (windows, dialog) number 60 MariaDB SQL table number 38 MariaDB SQL table column number 320 Source lines of code (SLOC) 300,000 1.1 Motivations This paper describes an effective dynamic analysis framework, based on runtime monitors specified in C++ programs (implemented in the software library yri_sd_runtime_verif), to perform software temporal safety property checking of GUI (Graphical User Interface) based software. GUI based software are very comfortable and handy to use. However, tools to perform temporal safety property verification of GUI software are allmost not available as FOSS. The testing of combinations between GUI windows and database queries that glue them to make sense to the user, is allmost unavailable as FOSS, or at all to the best of the knowledge of the author of this paper. The FOSS C++ library libfsmtest [7] provides test suite generation support for source code behavior specifications as mealy automata. However, libfsmtest only allows for desirable correctness properties, and doesn’t provide GUI (interaction) support or as plugin-based. Unit or integration testing for GUI widgets is available by use of "NUnit" testing frameworks like e.g. QtTest [8], CppUnit [9], etc.. Software testing across GUI widgets (and MySQL queries) is however limited in support by these "NUnit" framework. To the best of the knowledge of the author of this paper, DejaVu [10] provides some support for Java’record and replay’ testing while FROGLOGIC [11] provides support for C++ GUI software ’record and replay’ testing technology. ’Record and replay’ testing means a user performs a sequence of events that are recorded by testing infrastructure and automatically replay later on to see if expected events thereof occur. However, none of this ’record and replay’ technology tool enable temporal safety property specification as FOSS, with SQL as plugin. 2 As we will see in the related work, section 7, of this paper, most of software correctness property checking frameworks don’t put an emphasis on checking temporal safety property of GUI software. Characterizing the effects of program statements (via SQL statements) on database table columns, and to check that these characteristics hold or not, is of predominant importance for large software systems with an impressive number of database tables. Table 1illustrates for instance FOSS YERITH–ERP–3.0 relevant software system metrics. It means it can be very difficult for developers to keep application related logical requirements between the tables without appropriate software testing or analysis tools. A large amount of former work on runtime monitoring assumes for a sequential program, or an abstraction of the program as one single source code, on which program analysis is performed [12– 16]. The program analysis technique the author of this paper presents here abstract SQL events, GUI events, or sequences of them, as a state diagram, and enables developers to run them sequentially against a runtime monitor specified as a C++ program. In particular, the example presented in Section 3specifies results of GUI windows events as SQL database pre-conditions on state diagram transitions; SQL events are specified as state diagram transition events. Figure 1shows a high level overview of YRIDBRUNTIMEVERIF workflow. 1.2 Main Contributions This paper presents 3original main contributions: •an industrial level quality framework (YRIDBRUNTIMEVERIF:https://github.com/ yerithrd/yri-db-runtime-verif), that solves temporal property verification by dynamic program analysis. YRIDBRUNTIMEVERIF makes use of the C++ QtDbus library, to input a runtime monitor specification (yri_sd_runtime_verif)as C++ program code, that also enables software–library–plugin checks; •aC++ library: yri_sd_runtime_verif (https://github.com/yerithrd/yri_sd_ runtime_verif); modeling a state diagram runtime monitoring interface using only set algebra inclusion operations (∈, /∈) for state diagram program state specification as preand post-conditions. yri_sd_runtime_verif only enables the specification of states diagrams specifications as not desirable (forbidden) behavior specifications (fail traces). Thus, YRIDBRUNTIMEVERIF doesn’t generate any false warning. A violation of a safety rule has been found whenever a final state could be reached. On the other hand, not reaching a final state doesn’t mean that there is not a test case (or test input) that cannot reach this final state. •An application of YRIDBRUNTIMEVERIF to check 1temporal safety property error, found in the ERP FOSS YERITH–ERP–3.0. Previous version of this paper This paper extends a previous version [17], currently in conference proceedings SPLASH– ICTSS 2023 submission, with state diagram with more than 2states, guarded conditions specifications, 2new keywords for state diagram transition trace specification (”in_sql_event_log”, ”not_in_sql_event_log”), 2 new keywords (”IN_POST_NOP”, ”NOT_IN_POST_NOP”) for no-operations state post-conditions; And YRIDBRUNTIMEVERIF binaries with more than 1runtime monitor. 1.3 Overview This paper is organized as follows: Section 2 presents formal definitions of the principal concepts used in this paper. Section 3presents a motivating example that will be used throughout this paper to explain the presented concepts of this paper. Section 4presents the software architecture of YRIDBRUNTIMEVERIF, our GUI dynamic analysis framework. Section 5introduces the C++ software library yri_sd_runtime_verif to model states diagrams, and reused by YRIDBRUNTIMEVERIF. We evaluate our dynamic runtime analysis in Section 6. Section 7compares this paper with other papers that achieve similar work or endeavors. Section 8concludes this paper. 3 2 Formal Definitions yri_sd_runtime_verif’s formal description of the state diagram formalism follows Mealy machine [3] added with accepting states (final or erroneous states), and state diagram transition preand post-conditions: ”state diagram mealy machine”. Another excellent, detailed with proofs and theory presentation of mealy automata [18] is available. In comparison to statechart [19], which is a visual formalism for states diagrams, yri_sd_runtime_verif doesn’t support at time for instance the following features: hierarchical states (composite state, submachine state), timing conditions (timing conditions on states entries, and / or transition triggering conditions). Definition 1: A state diagram. A state diagram is an 8–tuple (S, S0, C, Σ,Λ, δ, T, Γ) where: •S: a finite set of states •S0∈S: a start state (or initial state) •C: a set of predicate conditions; preconditions are underlined (e.g.: Q0), and post-conditions are overlined (e.g.: Q1). A pre-condition is comparable to a Harelstatechart guarded condition. •Σ: an input alphabet, Σ:= {False, True}. ′False′means no input from SUT into YRIDBRUNTIMEVERIF. ′True′means any input could come from SUT. •Λ: an output alphabet (of program events en(n∈N)), φthe no program event. A program event generally corresponds to a function or method call at a SUT source code statement (or program point). •δ:S×C: a 2-ary relation that maps a state sto a state-condition cas either a state diagram transition pre-condition (c), or as a state diagram transition post-condition (c). •T:S×Σ→S×Λ: a transition function that maps an input symbol to an output symbol and the next state. •: a 2−ary relation that maps a state diagram transition to a guarded condition expression. •Γ: a set of accepting states; Γ∈S. For instance, for the motivating example described in Figure 2we have: •S={D,E}; •S0=D; •C={Q0, Q1}; •Σ={F alse, T rue}; •Λ={φ, ’SELECT.department’}; •δ={(D, Q0),(E, Q1)}; •T={((D, F alse),(D, φ)),((D, T rue),(E,’SELECT.department’))}; •Γ={E} Definition 2: A pre-condition. A pre-condition of a state diagram transition is a predicate that must be true before the transition can be triggered. A pre-condition Q0could have 2forms: •Q0:= IN_PRE(X, Y) that means value "X" is in (∈) database column value set "Y". •Q0:= NOT_IN_PRE(X, Y) that means value "X" is not in (/∈) database column value set "Y". Definition 3: A post-condition. A post-condition of a state diagram transition is a predicate that must be true after the transition was triggered. A post-condition Q1could have 2 forms: •Q1 := IN_POST(A, B) that means value "A" is in (∈) database column value set "B". •Q1 := NOT_IN_POST(A, B) that means value "A" is not in (/∈) database column value set "B". For state diagram mealy machines with more than 2states, only the first transition has a pre-condition specification (IN_PRE, or NOT_IN_PRE). Each other transition only has a post-condition specification (IN_POST, or NOT_IN_POST). Since each state only has 1outgoing (edge) state transition, the postcondition of the previous (incoming) state transition acts as the pre-condition of the next transition. IT is also for user interest to have following NO–OPeration post-conditions when working with state diagram mealy machines with more than 2states : ◦IN_POST_NOP 4 ◦NOT_IN_POST_NOP OUR experience, not reported at time anywhere, shows that state diagram mealy machine with more than 2states are really more for parallel system modeling; I.E. systems that work in GUI with timers and several threads of work at anytime. “In such cases, subsequent linearly placed states may not belong to same thread of execution: this is kind of what is called in CSP (Communicating Sequential Processes) []; Parallel Composition.“ Definition 4: A trace. A trace Tn=< e0, e1, .., en>is a sequence of SUT events (or SUT program points) ei,i∈{0,..,n} of length n.trace(D)is the trace of SUT events up to state D. For instance, for the motivating example described in Figure 2we have: trace(E) = trace(D), < ’SELECT.department’>. Proposition 1: NO FALSE WARNINGS. yri_sd_runtime_verif only allows 1outgoing edge or transition for a state in its specifications, and for not desirable (forbidden) behavior, as illustrated in Figure 2. There is no need to specify the red colored edge in Figure 2because it represents runtime cases where no input events arrive from SUT into YRIDBRUNTIMEVERIF. These 2properties, together with algorithm ’YRI_trigger_an_edge_event(QString an_edge_event)’ (Listing 3) of yri_sd_runtime_verif, ensures that there are no false warnings during YRIDBRUNTIMEVERIF analyses. For example, the runtime monitoring or verification systems [12–16] may give false warnings. 2.1 Guarded Condition Expression Specification in yri_sd_runtime_verif Guarded conditions expressions can be specified using one of the yr_create_monitor_edge method and a boolean expression of type YR_CPP_BOOLEAN_expression. An edge without an explicit guarded condition has an implicit ’[True]’ guarded condition on it. The implicit guarded condition ’[True]’ mustn’t be identified as an implicit input event ’True’, as specified in Definition 1. Guarded conditions are meant to be trace set specification on program events. For instance in Figure 2(motivating example): "[in_set_trace (’DELETE.department.YRI_ASSET’, STATE(D))]"means that a SQL ’DELETE’ event removing a department named ’YRI_ASSET’ from MariaDB SQL table ’department’ must have occurred in the trace leading to state ’D’, before event ’SELECT.department’ can be triggered. A guarded condition could have two practical forms: •"[in_set_trace (’event’, STATE(D))]" is equivalent to: ’event’ ∈trace(D). •"[not_in_set_trace (’event’, STATE(D))]" is equivalent to: ’event’ /∈trace(D). where ’event’ is an input event (event ∈Σ) and ’D’ a state diagram state (D∈S). 5 Fig. 2: A motivating example, as current bug in YERITH–ERP–3.0. Q0 := NOT_IN_PRE(YRI_ASSET, department.department_name). Q1 := IN_POST(YRI_ASSET, stocks.department_name). D Q0 start E Q1 False / φ [in_set_trace(’DELETE.department.YRI_ASSET’, STATE(d))] / ’SELECT.department’ Fig. 3:YERITH–ERP–3.0 administration section displaying departments (¬Q0). Fig. 4:YERITH–ERP–3.0 stock asset window listing some assets (Q1). 3 Motivating Example: missing department definition 3.1 The Enterprise Resource Planing Software YERITH–ERP–3.0 YERITH–ERP–3.0 is a fast, yet very simple in terms of usage, installation, and configuration Enterprise Resource Planing Software developed by Noundou et al. [5] for very small, small, medium, and large enterprises. YERITH–ERP– 3.0 is developed using C++ by means of the Qt development library. YERITH–ERP–3.0 is a large software with around 300 000 (three hundred thousands) of physical source lines of code. YRIDBRUNTIMEVERIF could be used for integration testing of YERITH–ERP–3.0, among different software modules. 3.2 Example Temporal Safety Property The motivating example of this paper consists of the temporal safety property stipulating that ”A DEPARTMENT SHALL NOT BE DELETED WHENEVER STOCKS ASSET STILL EXISTS UNDER THIS DEPARTMENT”. This statement means that a user shall be denied the removal of department ’YRI_ASSET’ in Figure 3because there are still a stock asset listed within department ’YRI_ASSET’, as illustrated in Figure 4. Figure 2 6 Fig. 5:YRIDBRUNTIMEVERIF graphical EDITOR viewing interface demonstrating that a final state has been reached (Section 6analyzes these results). illustrates the above temporal safety property as a simple state diagram. 3.2.1 State Diagram Explanation ’D’ is a start state as illustrated by an arrow ending on its state shape. ’E’ is a final (error, or accepting) state as illustrated by a double circle as state shape. The pre-condition Q0(as a predicate) in state ’D’: "NOT_IN_PRE(YRI_ASSET, department.department_name)" means: •a department named ’YRI_ASSET’ is not in column ’department_name’ of MariaDB SQL database table ’department’. This might happen whenever button ’Delete’ in Figure 3is pressed when item ’YRI_ASSET’ is selected. Similarly, the post-condition Q1(as a predicate) "IN_POST(YRI_ASSET, stocks.department_name)", in accepting state ’E’, means: •a department named ’YRI_ASSET’ is in column ”department_name’’ of MariaDB SQL database table ’stocks’. The state diagram event transition in Figure 2: ’SELECT.department’ denotes that when in ’D’, a SQL ’select’ on database table ”department’’ has occurred; ’E’ is then reached as an accepting state. 7 Guarded Condition Expression The guarded condition expression "[in_set_trace (’DELETE.department.YRI_ASSET’, STATE(D))]"means a SQL ’DELETE’ event removing a department named ’YRI_ASSET’ from MariaDB SQL table ’department’ must have occurred in the trace leading to state ’D’. Yri_sd_runtime_verif Specification Code The source code specified in Listing 2also illustrates a specification in C++ using software library yri_sd_runtime_verif of the state diagram specification above. 3.3 YRIDBRUNTIMEVERIF Analysis Report The motivating example automaton in Figure 2is analyzed by YRIDBRUNTIMEVERIF as follows: •whenever department ’YRI_ASSET’ is deleted in YERITH–ERP–3.0, as done in Figure 3, the runtime monitor state ’D’ with a state condition Q0is entered •when MySQL library (plugin) event ’SELECT.department’ occurs, in Figure 3 because of YERITH–ERP–3.0 displaying the remaining product departments, the guarded condition for edge event ’SELECT.department’ is automatically evaluated to ’True’ by C++ library yri_sd_runtime_verif, because no other guarded condition was specified by the developer •yri_sd_runtime_verif enters the runtime monitor state to ’E’ and state condition Q1via method YRI_trigger_an_edge_event(QString an_edge_event) because there are still assets (yerith_asset_3) left within product department ’YRI_ASSET’, as illustrated in Figure 4. ’E’ is then an accepting (or final or error) state. Figure 5illustrates an analysis result of the afore described process, which gets evaluated and described in Evaluation Section 6. 8 7 Related Work •SUT source code instrumentation with runtime monitor specification. "Clara" [12] enables to express software correctness properties using AspectJ and dependency state machines (related to tracematches [21]), both as instances of the typestate formalism, a formalism that is merely used for checking correctness of programs by a static compilation (analysis) technique called typestate checking. The Clara framework weaves (instruments), and annotates a program with runtime monitors using AspectJ, then tries to optimize the weaved program by static analysis. The ”residual program”, meaning the weaved statically optimized program is then executed and runtime monitored by developers to detect runtime errors. Runtime monitoring tools [13–16] work as similar as the Clara framework does. YRIDBRUNTIMEVERIF doesn’t instrument the System Under Test (SUT) with any specification. It runs the runtime monitor concurrently from the analyzed SUT, but not with hand–shaking mechanism, thus not increasing runtime execution of the SUT. YRIDBRUNTIMEVERIF specifies the runtime monitor as a state diagram mealy machine, a subset of typestate, specified as a C++ program, and extended with accepting states and state transition preand post-condition. •SUT binary code instrumentation with a runtime monitor. With tracerory [6, 22]", Jon Eyolfson and Patrick Lam use runtime program binary code instrumentation technique in INTELpin [23] to instrument running programs for purposes of detecting unread memory. I.e., tracerory doesn’t generate itself a runtime monitor, it uses INTELpin [23] to generate a runtime monitor for its verification purposes. "Purify" [24] doesn’t allow for SUT user correctness property specification. It has built-in memory access safety properties to check offline on program execution, after instrumentation of the SUT, its third-party, and vendor object-code libraries. In contrast, with YRIDBRUNTIMEVERIF, the user instruments the source code of the analyzed C++ program at compile time with SQL events emitting code. YRIDBRUNTIMEVERIF could also be used to perform memory write integrity check like tracerory.YRIDBRUNTIMEVERIF monitors program trace events at database level (also source code statement level by mapping to SQL query statements), and not at program counter level as tracerory does. YRIDBRUNTIMEVERIF inputs a SUT correctness property specification as a state diagram mealy machine (as a subset of LTL [2]); YRIDBRUNTIMEVERIF is a runtime monitor container; YRIDBRUNTIMEVERIF also generates itself a runtime monitor whereas tracerory doesn’t. •Source code automated test case generation for C++ with TDIOHS [25], or FOSS library libfsmtest [7]. ”Peleska et al.” created a Framework for generating Harel– statecharts fully compatible state diagrams as Test programs as C++ object–oriented program code; Based on ”Peleska et al.” formalism of Time Discrete Input/Output Hybrid System (TDIOHS). TDIOHS models state systems that handle real and discrete real number data as input to the system under test; TDIOHS models SUT execution by a so called SYMBOLIC TEST CASES TREE (STCT) that represents all possible runtime execution paths of the SUT by means of symbolic test cases data. Symbolic test cases data are data that cannot be used in a runtime execution, BUT that are generated outside from STCT tree by a symbolic test data generator algorithm. The SUT sample tree execution paths are then traversed based on the real test data generated by a symbolic test data generator component [26]. In contrast, the framework YERITH_QVGE runtime monitors a program under analysis only for specified fail (forbidden) trace behaviors as given by users. •Specification as set interface operations. "Hob" [27,28] is a program verification framework that enables to: characterize effects of program statement on data 15 structures by means of all (∀,∃,etc.) algebra abstract set interface operations; and to check that these characteristics hold or not, using static analyses. YRIDBRUNTIMEVERIF is a program verification framework that enables to: characterize effects of program statements via SQL [4] (Structure Query Language) on database table columns by means of set interface operations (∈, /∈); and to check that these characteristics hold or not, using dynamic runtime analysis. •Concurrent Event Stream Analysis. "DejaVu" [29] enables to check safety temporal property expressed in first-order past linear-time temporal logic (FOPLTL) for events that carry data. DejaVu inputs a trace log (offline) and a FOPLTL formula, and outputs a boolean value for each position in the inputted trace. "LogScope" [30] checks, offline, software systems correctness properties expressed using a rule–based specification language over state machines. It is not very precise what type of state machine is created and processed. "LogScope" translates specifications into C++ monitors (that could carry data). "EventRaceCommander" [31] repairs in web applications (online), event race errors, a kind of safety error. States diagrams specifications are implemented as C++ program monitors using C++ library yri_sd_runtime_verif. YRIDBRUNTIMEVERIF outputs a developer given (by means of a callback function, as seen in ’line 15’ in Listing 2) string message 1 in case an accepting state was entered, and a trace event of YERITH–ERP–3.0 leading to it. YRIDBRUNTIMEVERIF’s monitors need not store data, as DejaVu monitors must. YRIDBRUNTIMEVERIF events also carry data (database table and column name, records quantity modified by current SUT event). Runtime monitors could be checked against programs written in any programming language or framework, as 1’YRI_DB_RUNTIME_VERIF_Monitor_notify_SUCCESS_VERIFICATION’ in this paper motivating example in Figure 5. long as they emit necessary SQL events to YRIDBRUNTIMEVERIF. 16 Fig. 11:A Mealy Machine State Diagram Specified Using yri_sd_runtime_verif Specification Language. 1. yri_sd_mealy_automaton_spec yri_missing_department 2. { 3. START_STATE(d):NOT_IN_PRE(YRI_ASSET,department.department_name) 4. ->[in_sql_event_log(’DELETE.departement.YRI_ASSET’,STATE(d))]/’SELECT.department’-> 5. ERROR_STATE(e):IN_POST(YRI_ASSET,stocks.department_name). 6. } Fig. 12: ’YERITH_QVGE’ model for the example specification in Figure 11. 8 Conclusion And Future Work This paper has presented a lightweight C++ QtDbus [32] tool to check a program against a runtime monitor using set interface operations (∈, /∈) on program statement: YRIDBRUNTIMEVERIF. YRIDBRUNTIMEVERIF doesn’t generate false warnings; YRIDBRUNTIMEVERIF specifications are not desirable (forbidden) specifications (fail traces). Since the concurrent communication between YRIDBRUNTIMEVERIF and a program occurs over the RPC (Remote Procedure Call) instance Dbus, a runtime monitor could be checked against programs written in any programming language or framework, as long as they emit the necessary SQL events to YRIDBRUNTIMEVERIF. Future work would be a tool-chain to validate yri_sd_runtime_verif models as represented in this paper. Also, the author of this paper has developed a graphical drawing tool (YERITH_QVGE) for in Section 2defined state diagrams. A model of YERITH_QVGE is shown in Figure 12. It is an extension of the FOSS (Free and Open Source Software) Qt Graphviz [33] drawing tool QVGE [34]. YERITH_QVGE generates, from a model, an input file for the compiler yri_sd_runtime_verif_lang_comp. 17 Listing 4: ’DO_VERIFY_AND_or_CHECK_ltl_PROPERTY’: YRIDBRUNTIMEVERIF’s overridden method for processing SUT event stream C++ pseudo-code. 1bool DO_VERIFY_AND_or_CHECK_ltl_PROPERTY( 2 QString sql_table_NAME, 3 SQL_CONSTANT_IDENTIFIER cur_SQL_command) 4 { 5switch (cur_SQL_command) 6 { 7case SELECT: 8 9if ("department" == sql_table_NAME)) 10 { 11 return YRI_trigger_an_edge_event("’select.department’"); 12 } 13 break; 14 15 default: 16 break; 17 } 18 19 return false; 20 } A Processing of SUT Event Stream By An Analysis Client Listing 4illustrates the pseudocode of YRIDBRUNTIMEVERIF SUT event processing method ’DO_VERIFY_AND_or_CHECK_ltl_PROPERTY’. An analysis client must first override method ’DO_VERIFY_AND_or_CHECK_ltl_PROPERTY’ of class ’YRI_DB_RUNTIME_VERIF_Monitor’ so to implement a checking algorithm for each event received from SUT, as for instance the events illustrated in Figure 2of the motivating example. The analysis client then calls method ’YRI_trigger_an_edge_event(QString an_edge_event)’ of class ’YRI_CPP_RUNTIME_MONITOR’ of C++ library yri_sd_runtime_verif for each corresponding state diagram transition event. B YRI_SD_RUNTIME_VERIF SPECIFICATION LANGUAGE 18 Fig. 13:Grammar in Backus–Naur Form (BNF) of yri_sd_runtime_verif Mealy Machine State Diagram Specification Language. hspecificationi::= yri_sd_mealy_automaton_spec ’{’ hmealy-automaton-speci’.’ ’}’ hmealy-automaton-speci::= hsut-state-speci |hsut-state-speci’→’hsut-edge-state-speci hsut-edge-state-speci::= hsut-edge-mealy-automaton-speci’→’hmealy-automaton-speci hsut-edge-mealy-automaton-speci::= hedge-mealy-automaton-guard-condi hevent-calli hedge-mealy-automaton-guard-condi::= /* empty */ ’/’ | ’[’ htrace-specificationi’]’ ’/’ htrace-specificationi::= hin-sql-event-logi|hnot-in-sql-event-logi|hin-set-tracei|hnot-in-set-tracei hsut-state-speci::= hstart-state-property-speci |hstart-state-property-speci’:’ halgebra-set-specificationi |hstate-property-speci’:’ halgebra-set-specificationi |hfinal-state-property-speci’:’ halgebra-set-specificationi |hfinal-state-auto-property-speci’:’ halgebra-set-specificationi’:’ hrecovery-sql-query-speci halgebra-set-specificationi::= hin-algebra-set-speci|hnot-in-algebra-set-speci hin-algebra-set-speci::= hin-speci’(’ hprog-variablei’,’ hdb-tablei’.’ hdb-columni’)’ |hin-spec-nopi’(’ ’)’ hnot-in-algebra-set-speci::= hnot-in-speci’(’ hprog-variablei’,’ hdb-tablei’.’ hdb-columni’)’ |hnot-in-spec-nopi’(’ ’)’ hin-sql-event-logi::= in_sql_event_log’(’ hevent-calli’,’ hstate-property-specificationi’)’ hnot-in-sql-event-logi::= not_in_sql_event_log’(’ hevent-calli’,’ hstate-property-specificationi’)’ hin-set-tracei::= in_set_trace’(’ hevent-calli’,’ hstate-property-specificationi’)’ hnot-in-set-tracei::= not_in_set_trace’(’ hevent-calli’,’ hstate-property-specificationi’)’ hin-speci::= IN_BEFORE |IN_AFTER |IN_PRE |IN_POST hin-spec-nopi::= IN_POST_NOP hnot-in-speci::= NOT_IN_BEFORE |NOT_IN_AFTER |NOT_IN_PRE |NOT_IN_POST hnot-in-spec-nopi::= NOT_IN_POST_NOP hstart-state-property-speci::= START_STATE’(’ AlphaNum ’)’ hstate-property-speci::= STATE’(’ AlphaNum ’)’ hfinal-state-property-speci::= END_STATE’(’ AlphaNum ’)’ |FINAL_STATE’(’ AlphaNum ’)’ |ERROR_STATE’(’ AlphaNum ’)’ hfinal-state-auto-property-speci::= END_STATE_AUTO’(’ AlphaNum ’)’ |FINAL_STATE_AUTO’(’ AlphaNum ’)’ |ERROR_STATE_AUTO’(’ AlphaNum ’)’ hrecovery-sql-query-speci::= recovery_sql_query’(’ hdb-tablei’,’ hsql-recovery-queryi’)’ hsql-recovery-queryi::= String hevent-calli::= String hprog-variablei::= AlphaNum hdb-tablei::= AlphaNum hdb-columni::= AlphaNum 19 Fig. 14:YERITH–ERP–3.0 Maintenance Verification Interface. C YERITH–ERP–3.0 MAINTENANCE VERIFICATION INTERFACE 20 References [1] Wikipedia.org: SQL - Wikipedia. https://en. wikipedia.org/wiki/SQL. Accessed last time on February 08,2023 at 12:00 (2023) [2] Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd Edition. (2018). https://mitpress.mit. edu/books/model-checking-second-edition [3] Wikipedia.org: Mealy machine. https: //en.wikipedia.org/wiki/Mealy_machine. Accessed last time on Dec 15,2022 at 12:00 (2022) [4] MariaDB.org: MariaDB Foundation - MariaDB.org. https://www.mariadb.org. Accessed last time on June 24,2022 at 12:20 (2022) [5] Noundou, X.: YERITH–ERP–PGI–3.0 Doctoral Compendium. https://archive.org/ download/yerith-erp-pgi-compendium_ 202206/JH_NISSI_ERP_PGI_ COMPENDIUM.pdf. Accessed last time on January 21,2023 at 23:24 (2022) [6] Eyolfson, J., Lam, P.: Detecting unread memory using dynamic binary translation. In: Qadeer, S., Tasiran, S. (eds.) Runtime Verification, pp. 49–63. Springer, Berlin, Heidelberg (2013) [7] Bergenthal, M., Krafczyk, N., Peleska, J., Sachtleben, R.: libfsmtest an open source library for fsm-based testing. In: Clark, D., Menendez, H., Cavalli, A.R. (eds.) Testing Software and Systems, pp. 3–19. Springer, Cham (2022) [8] doc.qt.io/qt-5: Qt 5.15.https://doc.qt.io/ qt-5. Accessed last time on Dec 22,2022 at 12:40 (2022) [9] https://freedesktop.org/wiki/Software/cppunit: cppunit. https://doc.qt.io/qt-5/ qtdbus-index.html. Accessed last time on January 01,2023 at 12:00 (2022) [10] Alpern, B., Ngo, T., Choi, J.-D., Sridharan, M.: DejaVu: deterministic Java replay debugger for Jalapeño Java virtual machine. In: Addendum to the Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (2000). https://doi.org/10.1145/ 367845.368073 [11] froglogic.com: Home •froglogic. https:// www.froglogic.com/home. Accessed last time on Dec 18,2022 at 20:00 (2022) [12] Bodden, E., Hendren, L.: 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 [13] Butkevich, S., Renedo, M., Baumgartner, G., Young, M.: Compiler and tool support for debugging object protocols. In: SIGSOFT ’00/FSE-8 (2000) [14] Allan, C., Avgustinov, P., Christensen, A.S., Dufour, B., Goard, C., Hendren, L.J., Kuzins, S., Lhoták, J., Lhoták, O., Moor, O., Sereni, D., Sittampalam, G., Tibble, J., Verbrugge, C.: abc the aspectbench compiler for aspectj a workbench for aspect-oriented programming language and compilers research. In: Johnson, R.E., Gabriel, R.P. (eds.) Companion to the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, October 16-20, 2005, San Diego, CA, USA, pp. 88–89. ACM, ??? (2005). https://doi.org/10.1145/1094855.1094877 . https://doi.org/10.1145/1094855.1094877 [15] Bodden, E.: J-LO - A tool for runtimechecking temporal assertions. Diploma thesis, RWTH Aachen University (November 2005). https://www.bodden.de/pubs/ bodden05jlo.pdf [16] Chen, F., Rosu, G.: Mop: an efficient and generic runtime verification framework. In: Gabriel, R.P., Bacon, D.F., Lopes, C.V., Jr., G.L.S. (eds.) Proceedings of the 22nd Conference on Object-Oriented Programming, Systems, Languages and Applications, pp. 569–588. ACM, ??? (2007). https://doi.org/ 10.1145/1297027.1297069 21 [17] Noundou, X.: Yr_db_runtime_verif: a framework for verifying sql correctness properties of gui software at runtime (2023). https://archive.org/download/yri_ictss_ 2023/yri_ictss_2023.pdf [18] Peleska, J., Huang, W.-l.: Test Automation; Foundations and Applications of Model-based Testing. https: //www.informatik.uni-bremen.de/agbs/jp/ papers/test-automation-huang-peleska.pdf. Accessed last time on May 06,2023 at 12:00 (2021) [19] Harel, D.: Statecharts: a visual formalism for complex systems. Science of Computer Programming 8(3) (1987) [20] Booch, G., Rumbaugh, J., Jacobson, I.: Unified Modeling Language User Guide, The (2nd Edition) (Addison-Wesley Object Technology Series). (2005) [21] Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to aspectj. In: OOPSLA ’05 (2005) [22] Eyolfson, J.: Tracerory; Dynamic Tracematches and Unread Memory Detection for C/C++. (2012). MASTER OF APPLIED SCIENCES (MASc). https://hdl.handle.net/ 10012/6206 [23] Luk, C.K., Cohn, R.S., Muth, R., Patil, H., Klauser, A., Lowney, P.G., Wallace, S., Reddi, V.J., Hazelwood, K.M.: Pin: building customized program analysis tools with dynamic instrumentation. In: PLDI ’05 (2005) [24] Hastings, R.O., Joyce, B.A.: Fast detection of memory leaks and access errors. (1991) [25] Badban, B., Fränzle, M., Peleska, J., Teige, T.: Test automation for hybrid systems. In: Third International Workshop on Software Quality Assurance (SOQUA 2006), pp. 14–21 (2006) [26] fopoussi, S.A.: Test data ... In: DISSERTATION in INFORMATIK (2010) [27] Kuncak, V., Lam, P., Zee, K., Rinard, M.: Modular pluggable analyses for data structure consistency. Transactions on Software Engineering 32(12), 988–1005 (2006) [28] Lam, P.: The Hob System for Verifying Software Design Properties. (2007) [29] Havelund, K., Peled, D., Ulus, D.: Dejavu: A monitoring tool for first-order temporal logic, pp. 12–13 (2018). https://doi.org/10. 1109/MT-CPS.2018.00013 [30] Havelund, K.: Specification-based monitoring in c++. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, pp. 65–87. Springer, Cham (2022) [31] Adamsen, C.Q., Møller, A., Karim, R., Sridharan, M., Tip, F., Sen, K.: Repairing event race errors by controlling nondeterminism. In: Proceedings of the 39th International Conference on Software Engineering, ICSE (2017). https://doi.org/10.1109/ICSE. 2017.34 .files/ICSE17Repairing.pdf [32] doc.qt.io/qt-5/qtdbus-index.html: Qt D-Bus. https://doc.qt.io/qt-5/qtdbus-index.html. Accessed last time on Dec 22,2022 at 12:40 (2022) [33] graphviz.org: DOT Language | Graphviz. https://graphviz.org/doc/info/lang.html. Accessed last time on JUNE 8,2022 at 12:30 (2022) [34] showroom.qt.io: QVGE; Qt Visual Graph Editor | Showroom. https://showroom.qt. io/qvge-qt-visual-graph-editor. Accessed last time on Jun 27,2022 at 12:40 (2022) 22