YERITH_QVGE : A Framework for Verifying SQL Correctness Temporal Properties of [GUI] Software at Runtime

YERITH_QVGE : A Framework for Verifying SQL Correctness Temporal Properties of [GUI] Software at Runtime Xavier noumbissi Noundou1 1Yaounde, Center region, Cameroon. Contributing authors: y[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, Σ:= {F alse, 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 ’T rue’, 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 Fig. 6:YRIDBRUNTIMEVERIF: simplified software system architecture. OPERATING SYSTEM (OS) SUT (YERITH−ERP−3.0) LIBRARY − PLUGIN MYSQL library methods calls OS system calls yri−db−runtime−verif SUT source code instrumented QT socket calls (via Qt−Dbus) A RUNTIME MONITOR Fig. 7: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) Diagram from CASE tool (e.g.: YERITH_QVGE) 4 The Software Architecture of YRI-DB-RUNTIME-VERIF 4.1 Dynamic Analysis 4.1.1 SUT Source Code Instrumentation. YRIDBRUNTIMEVERIF runs as a separate Debian Linux process from the application to dynamically analyze (YERITH–ERP–3.0 in this case). Figure 6illustrates a software system architecture layer of a software system that uses YRIDBRUNTIMEVERIF. Figure 6and Figure 7illustrate how YERITH–ERP–3.0 is instrumented to send MySQL database events, as they occur on due to the GUI of YERITH–ERP–3.0, to process YRIDBRUNTIMEVERIF, so it can perform runtime analysis of the monitor implemented within it. 4.1.2 Debugging Information. Each GUI manipulation of YERITH–ERP–3.0 in its instrumented source code part could generate a state transition within the analyzed runtime monitor state diagram in YRIDBRUNTIMEVERIF. Visualize "line 35" of Figure 5to observe that a specific analysis message is sent to the console of YRIDBRUNTIMEVERIF in cases where a final state has been reached; the message at "line 33" is for an accepting (final) state of the state diagram specification of the motivating example presented in Figure 2. 4.2 SQL Events YRIDBRUNTIMEVERIF currently only processes the 4SQL events in Table 2. 4.3 A Runtime Monitor (An Analysis Client) Listing 1: "XML file adaptor for YERITH– ERP–3.0 test cases (reduced from 4to only 1SQL event for paper)." <!DOCTYPE node PUBLIC "−//freedesktop//DTD D−BUS Object Introspection 1.0//EN" "http://www.freedesktop.org/standards/dbus/1.0/introspect. dtd"> <node name="/YRruntimeverification"> <interface name="com.yerith.rd.IYRruntimeverification"> <method name="YRI_slot_refresh_SELECT_DB_MYSQL"> <annotation name="org.qtproject.QtDBus.QtTypeName.In0" value="QString"/> <annotation name="org.qtproject.QtDBus.QtTypeName.In1" value="uint"/> <annotation name="org.qtproject.QtDBus.QtTypeName.In2" value="bool"/> <arg type="QString" direction="in"/> <arg type="uint" direction="in"/> <arg type="bool" direction="out"/> </method> </interface> </node> An user (an analysis client) of YRIDBRUNTIMEVERIF needs to subclass class YR_DB_RUNTIME_VERIF_Monitor. The UML class diagram in Figure 8displays the class structure of YRIDBRUNTIMEVERIF.QtDbus communication adaptor IYRruntimeverificationAdaptor 9 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