YERITH_QVGE-de ini ions---chea --shee 2
YERITH_QVGE-use -guide 23
YERITH &d |Use ’s Chea Shee o YRI_SD_RUNTIME_VERIF : A C++ Func ional Lib a y o Speci ying ”SDMM” (S a e Diag am Mealy Machine)
Use ’s Chea Shee o
YRI_SD_RUNTIME_VERIF :
AC++ Func ional Lib a y o Speci ying
”SDMM” (S a e Diag am Mealy Machine)
AUTHOR: Xa ie Noundou [P . P o . D .–Ing. ]
Con ac : [email p o ec ed]
Con en s
Con en s 1
Lis o Figu es 2
Lis o Tables 3
1 Mo i a ion o SDMM’s Run ime Moni o ing Ve ifica ion Lib a y ”YRI_SD_RUNTIME_VERIF”6
1.1 A Sample Use–Case Scena io o ”SDMM”..................................................... 6
1.2 WHY DO I NEED FORMAL METHODS ....................................................... 6
1.2.1 ”C++ lib a y YRI_SD_RUNTIME_VERIF”: Exp essing o sequencing o ac ions in ime ( empo al usage ules o sys em
sa e y) ....................................................................... 6
1.3 Compa ison wi h Uni Tes ing ............................................................ 6
1.3.1 Uni Tes ing ................................................................... 6
1.3.2 Au oma ed Uni Tes ing ........................................................... 6
1.3.3 Run ime Moni o ing Ve ifica ion ...................................................... 6
1.4 S a e Diag am Mealy Machine : Usages & Ad an ages ............................................. 7
1.4.1 Usages ...................................................................... 7
1.4.2 Ad an ages ................................................................... 7
1.4.3 Cases o P ac ical Usages o ”SDMM” .................................................. 7
1.5 S a e Diag am Mealy Machine : B ie Summa y Explana ion ......................................... 7
1.6 Rela ed S a e Diag am Fo malisms ......................................................... 8
1.6.1 Da id Ha el S a echa : A Visual Fo malism o S a e Diag am .................................. 8
1.6.2 Timed Disc e e Inpu / Ou pu Hyb id Sys em (TDIOHS) ....................................... 8
1.6.3 TDIOHS in Ac ion wi hin ”Bo land Toge he 6”wi h RT–Tes e o ’ e ified.de’........................ 8
1.6.4 TDIOHS in Ac ion by ”Au oma ic Tes Cases / Da a Gene a ion” ................................. 9
2 Ma hema ical Fo mal Defini ion o SDMM 9
2.1 Defini ion 1: A s a e diag am ( o mealy machine). ............................................... 9
2.2 Defini ion 2: A p e-condi ion. ............................................................ 9
2.3 Defini ion 3: A pos -condi ion. ............................................................ 9
2.4 Defini ion 4: A ace. .................................................................. 10
2.5 SUT E en P ocessing Me hod YRI_ igge _an_edge_e en ................................... 10
2.5.1 P oposi ion 1: NO FALSE WARNINGS. .................................................. 10
2.5.2 Explana ion on HOW o a oid code ha c ea es False Wa nings (False Posi i es) ...................... 10
2.6 Gua ded Condi ion Exp ession Specifica ion in YRI_SD_RUNTIME_VERIF ................................... 10
2.7 SDMM o modeling pa allel-concu en so wa e sys em .......................................... 10
2.8 SDMM in Ac ion wi hin YRI_QVGE by ’Ye i h R&D’ ............................................... 10
2.9 SDMM in Ac ion by au oma ic ”Run ime Moni o s Au oma ic Gene a ion” ................................ 10
3 HOW TO Se up C++ Lib a y ”YRI_SD_RUNTIME_VERIF” o Usage in A C++ PROGRAM SOURCE CODE 10
3.1 De elopmen Toolchain ................................................................ 10
4 METHODS o C++ Lib a y ”YRI_SD_RUNTIME_VERIF”11
4.1 Gene a ed Me hod YOU need o code ....................................................... 11
5 A Ha dwa e Dedica ed De ice : YRI–QVGE–PC–Table 13
6 De ailed Scien ific and Enginee ing P esen a ion Documen on ’zenodo.o g’ 14
7 Conclusion 14
Index 14
Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "1 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Lis o Figu es
1 A mo i a ing example, as p e ious bug ound in YERITH–ERP–9.0.Q0 :=NOT_IN_BEFORE(YRI_ASSET, depa men .depa men _name) ; Q1 :=
IN_AFTER(YRI_ASSET, s ocks.depa men _name). ..................................................... 4
2 YERITH–ERP–9.0 adminis a ion sec ion displaying depa men s (¬Q0). ................................. 4
3 YERITH–ERP–9.0 s ock asse window lis ing some asse s (Q1). ....................................... 4
4A SAMPLE s a e diag am mealy machine file. KEYWORDS belonging bo h o ’enginee ing ("ERROR_STATE_AUTO")’,
and ’science (START_STATE)’ can be in e mingled in he same SDMM specifica ion file. ...................... 4
5 SAMPLE USE CASE SCENARIO OF "SDMM ". .................................................. 5
6 A SCREENSHOT OF YERITH_QVGE. ........................................................ 5
7 A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL EVENT LOG. ......................................... 5
9 A Sample Da id HAREL–S a echa model o he empo al p ope y exp essed in fig. 4 : —”Whene e depa men
YRI_ASSET was dele ed (e en ’DELETE.depa men .YRI_ASSET’); que ying s ock able shall no find again an in en o y
s ock in any depa men named YRI_ASSET”—. ................................................ 8
10 A STCT–symbolic es case ee andomly gene a ed by manual d awing o explana ion pu poses. ............... 8
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "2 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Lis o Tables
1 STATE DIAGRAM MEALY MACHINE SPECIFICATION KEYWORDS IN YERITH_QVGE. ’AUTO’ KEYWORDS SPECIFIES
ALSO SQL QUERY FOR GOING OUT AUTOMATICALLY FROM A FAIL (FORBIDDEN) STATE. (“SEE SECTION ??.“) ..... 4
2 Sample impo an Classes (p efix YRI_CPP_ o class name) & Me hods o C++ Lib a y ”YRI_SD_RUNTIME_VERIF”. ........ 11
3 YERITH_QVGE Toolchain ............................................................... 12
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "3 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Table 1: STATE DIAGRAM MEALY MACHINE SPECIFICATION KEYWORDS IN YERITH_QVGE. ’AUTO’ KEYWORDS SPECIFIES ALSO SQL QUERY FOR
GOING OUT AUTOMATICALLY FROM A FAIL (FORBIDDEN) STATE. (“SEE SECTION ??.“)
N◦scien ific keywo ds enginee ing keywo ds
1. in_se _ ace in_sql_e en _log
2. no _in_se _ ace no _in_sql_e en _log
3. eco e y_sql_que y eco e y_sql_que y
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
Figu e 1: A mo i a ing example, as p e ious bug ound in YERITH–ERP–9.0.
Q0:=NOT_IN_BEFORE(YRI_ASSET, depa men .depa men _name) ; Q1 :=IN_AFTER(YRI_ASSET, s ocks.depa men _name).
D
Q0
s a E
Q1
[in_sql_e en _log(’DELETE.depa men .YRI_ASSET’, STATE(D))] / ’SELECT.depa men ’
Figu e 2: YERITH–ERP–9.0 adminis a ion sec ion
displaying depa men s (¬Q0).
Figu e 3: YERITH–ERP–9.0 s ock asse
window lis ing some asse s (Q1).
Figu e 4: A SAMPLE s a e diag am mealy machine file. KEYWORDS belonging bo h o ’enginee ing ("ERROR_STATE_AUTO")’, and ’science
(START_STATE)’ can be in e mingled in he same SDMM specifica ion file.
1. y _sd_mealy_au oma on_spec y _missing_depa men _NO_DELETE
2. {
3. START_STATE(d):NOT_IN_BEFORE(YRI_ASSET,depa men .depa men _name)
4. ->[in_sql_e en _log(’DELETE.depa emen .YRI_ASSET’,STATE(d))]/’SELECT.depa men ’->
5. ERROR_STATE(e):IN_AFTER(YRI_ASSET,s ocks.depa men _name).
6. }
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "4 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Figu e 5: SAMPLE USE CASE SCENARIO OF "SDMM ".
In e ne
pa allel p ocess managemen
un ime execu ion and hea d
esou ces.
implemen YRI−DB−RUNTIME−VERIF
A PCI−CARD could also
(ne wo k) communica ion
QT−Dbus RPC P o ocol
execu es SDMM plugins
YRI−DB−RUNTIME−VERIF
NETWORK Rou e
(including Fi ewall)
YRI_QVGE CASE ool
d awing designs
A ailable also
in a USB dongle key
YRI−Db−Run ime−Ve i
Ja a De elope compu e unning
ela ed d awing designs
wi h In el−PIN)
(REQUIRES JVM e−ins umen a ion
Cybe −Secu i y SDMM
enables QT−plugin loading a un ime
YRI−DB−RUNTIME−VERIF
JVM−Ja a Vi ual Machine
IBM Websphe e APPLICATION Se e
/ O o e.g.: Que cus Applica ion Se e
se ing DYNAMIC / STATIC Web Apps
DBMS
Lis ing 1: Sample eal wo ld ”C++” code as opposed o PSEUDO–CODE ”C++” code; as modified by a de elope a e au oma ic gene a ion o YRI-DB-
RUNTIME-VERIF.
1bool YERITH_QVGE_sample_PAPER_ex ended_ e sion_PROPERY::DO_VERIFY_AND_o _CHECK_l l_PROPERTY(
2 QS ing sql_ able_ADDED_wi h_file_AND_line_numbe ,
3 uin sql_ eco d_q y_MODIFIED,
4 YRI_CPP_UTILS::SQL_CONSTANT_IDENTIFIER cu _SQL_command)
5 {
6 QS ingLis sql_ able_ADDED_wi h_file_AND_line_numbe _LIST = sql_ able_ADDED_wi h_file_AND_line_numbe .spli (";", Q ::KeepEmp yPa s);
7 QS ing sql_ able_name = sql_ able_ADDED_wi h_file_AND_line_numbe _LIST.a (0);
8 QS ing CPP_FILE_NAME = sql_ able_ADDED_wi h_file_AND_line_numbe _LIST.a (1);
9 QS ing cpp_line_numbe = sql_ able_ADDED_wi h_file_AND_line_numbe _LIST.a (2);
10
11 swi ch(cu _SQL_command)
12 {
13 case YRI_CPP_UTILS::INSERT:
14 b eak;
15
16 case YRI_CPP_UTILS::SELECT:
17 i (YRI_DB_RUNTIME_VERIF_U ils::isEqualsCaseInsensi i e(sql_ able_name, "depa emen s_p odui s")) {
18 e u n YRI_SQL_SELECT_depa emen s_p odui s();
19 }
20 b eak;
21
22 case YRI_CPP_UTILS::UPDATE:
23 b eak;
24
25 case YRI_CPP_UTILS::DELETE:
26 b eak;
27
28 de aul :
29 b eak;
30 }
31
32 e u n alse;
33 }
Figu e 6: A SCREENSHOT OF YERITH_QVGE.
Figu e 7: A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL
EVENT LOG.
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "5 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Table 3: YERITH_QVGE Toolchain
PROJECT Requi ed P og am / Lib a y
1)YRI_SD_RUNTIME_VERIF_LANG ”Q - oll ech” (h ps://doc.q .io/q -5)
2)YRI_SD_RUNTIME_VERIF_LANG_COMP 1)
3)YRI_SD_RUNTIME_VERIF_UNIT_TESTS 1)
4)YRI-DB-RUNTIME-VERIF 2)
Table 3illus a es o each lib a y p ojec , which o he s i depends on.
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "12 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
5 A Ha dwa e Dedica ed De ice : YRI–QVGE–PC–Table
A ha dwa e dedica ed de ice unning a un ime moni o ing
e ifica ion de ice called YRI–DB–RUNTIME–VERIF is in c ea ion by
mysel .
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "13 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
6 De ailed Scien ific and Enginee ing P esen a ion Documen
on ’zenodo.o g’
De ailed o mal scien ific and enginee ing con ibu ions o design
and es ing sys em YERITH_QVGE can be ound in JOURNAL
ARTICLE "Run ime Ve ifica ion O SQL Co ec ness P ope ies
wi h YRI-DB-RUNTIME-VERIF" [nN23].
7 Conclusion
The g aphical d awing ool YERITH_QVGE (Figu e 6) cos s only
2, 500 EUROS. WE ONLY SUPPORT DEBIAN–LINUX (h ps:
//www.debian.o g).
Re e ences
[AAC+05] Ch is Allan, Pa el A gus ino , Aske Simon
Ch is ensen, B uno Du ou , Ch is ophe Goa d,
Lau ie J. Hend en, Sascha Kuzins, Jenni e Lho ák,
Ond ej Lho ák, Oege de Moo , Damien Se eni,
Ganesh Si ampalam, Julian Tibble, and Cla k
Ve b ugge. abc he aspec bench compile o aspec j
a wo kbench o aspec -o ien ed p og amming
language and compile s esea ch. In Ralph E. Johnson
and Richa d P. Gab iel, edi o s, Companion o he
20 h Annual ACM SIGPLAN Con e ence on Objec -
O ien ed P og amming, Sys ems, Languages, and
Applica ions, OOPSLA 2005, Oc obe 16-20, 2005,
San Diego, CA, USA, pages 88–89. ACM, 2005.
[BFPT06] B. Badban, M. F änzle, J. Peleska, and T. Teige. Tes
au oma ion o hyb id sys ems. In Thi d In e na ional
Wo kshop on So wa e Quali y Assu ance (SOQUA
2006), pages 14–21, 2006.
[BH12] E ic Bodden and Lau ie Hend en. The cla a amewo k
o hyb id ypes a e analysis. In e na ional Jou nal
on So wa e Tools o Technology T ans e (STTT),
14:307–326, 2012. 10.1007/s10009-010-0183-5.
[Bod05] E ic Bodden. J-LO - A ool o un ime-checking
empo al asse ions. Diploma hesis, RWTH Aachen
Uni e si y, No embe 2005.
[BRBY00] Se gey Bu ke ich, Ma co Renedo, Ge ald
Baumga ne , and Michal Young. Compile and
ool suppo o debugging objec p o ocols. In
SIGSOFT ’00/FSE-8, 2000.
[CGK+18] Edmund M. Cla ke, O na G umbe g, Daniel K oening,
Do on A. Peled, and Helmu Vei h. Model checking,
2nd Edi ion, 2018.
[CR07] Feng Chen and G igo e Rosu. Mop: an efficien and
gene ic un ime e ifica ion amewo k. In Richa d P.
Gab iel, Da id F. Bacon, C is ina Videi a Lopes,
and Guy L. S eele J ., edi o s, P oceedings o he
22nd Con e ence on Objec -O ien ed P og amming,
Sys ems, Languages and Applica ions, pages 569–
588. ACM, 2007.
[Gau06] M.-C. Gaudel. ???– es au oma ion o hyb id
sys ems–??? In Thi d In e na ional Wo kshop on
So wa e Quali y Assu ance (SOQUA 2006), pages
14–21, 2006.
[Ha XX] Da id Ha el. S a echa s: a isual o malism o
complex sys ems. h ps://www.wisdom.
weizmann.ac.il/~dha el/SCANNED.
PAPERS/S a echa s.pd , XXXX. Accessed
las ime on Ap 28,2025 a 12:00.
[MYE20] And ew MYERS. So wa e es ing ..., 20..
[n 10] Se ges ACHILLES nono opoussi. Au oma isie e
es da engene ie ung hyb ide disk e -
kon inuie liche eingebe e e sys eme. h ps://
www.deu sche-digi ale-biblio hek.de/
pe son/gnd/141875240, 2010. DOCTORATE
THESIS IN COMPUTER SCIENCE (D .–Ing.),
Uni e si y o B emen, B emen, B emen, Ge many.
[NN07] Xa ie Noumbissi Noundou. S a is ical
es cases gene a ion o eac i e sys ems.
h ps://www.in o ma ik.uni-b emen.
de/agbs/quali ika ionsa bei en/
diploma bei en_e.h ml, 2007. In eg a ed
Bachelo & Mas e ’s Deg ee Thesis in Compu e
Science (B.Sc. & M.Sc.), Uni e si y o B emen,
B emen, B emen, Ge many.
[nN23] Xa ie noumbissi Noundou. A F amewo k o
Ve i ying SQL Co ec ness Tempo al P ope ies o
GUI So wa e a Run ime. h ps://zenodo.
o g/ eco ds/10976659, Oc obe 2023.
[NN25] Xa ie Noumbissi Noundou. A C++ unc ional
lib a y o speci ying "SDMM" (s a e diag am
mealy machine). h ps://www.zenodo.o g/
eco ds/10474033, 2025. A C++ Func ional
Lib a y o Speci ying "SDMM".
[Nou09] Xa ie Noundou. Juni 4 u o ial. h ps:
//www.zenodo.o g/ eco d/8052444,
Oc . 2009. Tex – u o ial ”Juni 4”, Uni e si y o
Wa e loo, Wa e loo, On a io, Canada.
[Nou22] Xa ie Noundou. YERITH–ERP–PGI–3.0 Doc o al
Compendium. h ps://a chi e.o g/
download/ye i h-e p-pgi-compendium_
202206/JH_NISSI_ERP_PGI_COMPENDIUM.
pd , June 2022. Accessed las ime on Janua y 21,
2023 a 23:24.
[PlH21] Jan Peleska and Wen ling Huang. Tes au oma ion;
ounda ions and applica ions o model-based
es ing. h ps://www.in o ma ik.
uni-b emen.de/agbs/jp/pape s/
es -au oma ion-huang-peleska.pd ,
July 2021. Accessed las ime on May 06,2023 a
12:00.
[Ra01] Bill Roscoe and al... CSP : Communica ing Sequen ial
P ocesses. UK, 2nd edi ion, 2001.
[Wik22] Wikipedia.o g. Mealy machine. h ps://en.
wikipedia.o g/wiki/Mealy_machine,
Decembe 2022. Accessed las ime on Dec 15,2022
a 12:00.
[Zel20] And eas Zelle . So wa e es ing ..., 20..
Index
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "14 / 16". | Ve sion o – June 1, 2025 –
JUni es ing amewo k, 6
A Sample Da id HAREL–S a echa model o he empo al
p ope y exp essed in fig. 4,8
A STCT–symbolic es case ee andomly gene a ed by manual
d awing o explana ion pu poses, 8
Au oma ed Uni Tes ing, 6
Black–box Tes ing, 6
Uni Tes ing, 6
Whi e–box Tes ing, 6
15
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "16 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "17 / 16". | Ve sion o – June 1, 2025 –
YRI_SD_RUNTIME_VERIF :C++ Func ional Lib a y o speci ying "SDMM"YERITH &d
Au ho : Xa ie Noundou [P . P o . D .–Ing. ] Holy-Ghos . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "18 / 16". | Ve sion o – June 1, 2025 –
YERITH &d |use ’s guide o YERITH_QVGE
Use ’s Guide o he
Design and Tes ing Sys em
YERITH_QVGE (YRI_QVGE)
AUTHOR: Xa ie Noumbissi Noundou [P . P o . D .–Ing. ]
Con ac : [email p o ec ed]
Con en s
Con en s 1
Lis o Figu es 2
Lis o Tables 3
1 In oduc ion 6
2 YERITH_QVGE (YRI_QVGE) Sho O e iew 6
3 YERITH_QVGE (YRI_QVGE) P ojec Dependency 7
4 Ad an ages o YERITH_QVGE 7
5 S a e Diag am Mealy Machine (SDMM) 7
5.1 HOW TO READ A "SDMM" .............................................................. 7
5.2 "SDMM" WITH MORE THAN 2STATES ...................................................... 7
6 YERITH_QVGE (YRI_QVGE) Wo kflow 7
7 Cus om Use P ojec (YRI–DB–RUNTIME–VERIF) 7
8 HOW TO START YRI-DB-RUNTIME-VERIF 8
9 SQL QUERY Reco e y execu ion on demand 8
9.1 Au oma ic SQL Command Que y Gene a ion .................................................. 8
9.1.1 ERROR ACCEPTING STATE o sdmm 1. ................................................ 9
9.1.2 RECOVERY 1. .................................................................. 9
9.1.3 RECOVERY 2 (P ac ical solu ion o be implemen ed in YRI-DB-RUNTIME-VERIF. ...................... 9
9.1.4 Conc e e RECOVERY 2 ac ion. ....................................................... 9
10 HOW TO USE a use in e ace 9
11 YRI_SD_RUNTIME_VERIF SPECIFICATION LANGUAGE 9
12 Fo mal Scien ific and Enginee ing P ojec Desc ip ion 9
13 Conclusion 9
Esp i –Sain . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "1 / 10". | Ve sion o – June 7, 2025 –
YERITH_QVGE use ’s guide YERITH &d
Lis o Figu es
1 A mo i a ingexample, asp e ious bug oundin YERITH–ERP–9.0.Q0 :=NOT_IN_BEFORE(YRI_ASSET, depa men .depa men _name); Q1 :=
IN_AFTER(YRI_ASSET, s ocks.depa men _name). ..................................................... 4
2 YERITH–ERP–9.0 adminis a ion sec ion displaying depa men s (¬Q0). ................................. 4
3 YERITH–ERP–9.0 s ock asse window lis ing some asse s (Q1). ....................................... 4
4A SAMPLE s a e diag am mealy machine file. KEYWORDS belonging bo h o ’enginee ing ("ERROR_STATE_AUTO")’,
and ’science (START_STATE)’ can be in e mingled in he same SDMM specifica ion file. ...................... 4
5 SAMPLE USE CASE SCENARIO OF "SDMM ". .................................................. 5
6 A SCREENSHOT OF YERITH_QVGE. ........................................................ 5
7 A SCREENSHOT OF YRI-DB-RUNTIME-VERIF SQL EVENT LOG. ....................................... 5
8 SOFTWARE ARCHITECTURE OF YRI-DB-RUNTIME-VERIF. ........................................ 6
9 YERITH_QVGE so wa e lib a y dependencies. ................................................. 6
10 Wo kflow explana ion. ................................................................. 7
11 SAMPLE sql eco e y s a e diag am model in YERITH_QVGE ........................................ 8
12 YERITH_QVGE use in e ace sc eensho . .................................................... 9
13 G amma in Backus–Nau Fo m (BNF) o YRI_SD_RUNTIME_VERIF_LANG Mealy Machine STATE DIAGRAM Specifica ion
Language. ......................................................................... 10
Au ho : Xa ie Noumbissi Noundou [P . P o . D .–Ing. ] Esp i –Sain . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "2 / 10". | Ve sion o – June 7, 2025 –
YERITH_QVGE use ’s guide YERITH &d
3 YERITH_QVGE (YRI_QVGE) P ojec Dependency
Table 2: YERITH_QVGE Design and Tes ing Sys em Dependencies
PROJECT Requi ed P og am / Lib a y
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 2illus a es o each lib a y p ojec , which o he s i depends
on.
4 Ad an ages o YERITH_QVGE
A sample s a e diag am mealy machine is shown in Figu e 4.
WITH manual d awing o SQL CORRECTNESS PROPERTY
MODEL, you a e eed om manually w i ing "s a e
diag am mealy machine ex files" ha could be edious and
leng hy. Also, edi ing s a e diag am mealy machine files
manually could be mo e e o -p one han le ing a compile
(YRI_SD_RUNTIME_VERIF_LANG) do i o you.
5 S a e Diag am Mealy Machine (SDMM)
TABLE 1depic s scien ific keywo ds and hei enginee ing
coun e pa ha can be used in desc ibing NOT DESIRABLE 3
SQL 4call sequence s a e diag am mealy machine in
YERITH_QVGE Design and Tes ing Sys em.
A STATE DIAGRAM mealy machine specifica ion is compiled
in o C++ code ha desc ibes a un ime moni o o be execu ed in
he un ime moni o ing es e YRI-DB-RUNTIME-VERIF. Figu e 4
depic s a sample S a e Diag am Mealy Machine specifica ion on
a NOT DESIRABLE SQL call sequence.
5.1 HOW TO READ A "SDMM"
Figu e 1shows a fini e au oma on ep esen a ion o he mealy
machine desc ip ion in Figu e 4. I shall be ead as ollows:
•Thep og amisinas a s a e D; s a e Disa s a s a e since
he e is incoming "START" a ow in o i .
•(P e-) Condi ion Q0: "depa men name ’YRI_ASSET’ is
no in able column ’depa men _name’ o da abase
able ’depa men ’"; applies in s a e D.
•Whene e GUARD CONDITION :
in_sql_e en _log(’DELETE.depa men .YRI_ASSET’,
STATE(d)): "e en ’DELETE.depa men .YRI_ASSET’
appea s in SQL e en log ( ace) leading o s a e
D"; applies in s a e D, sys em unde es (SUT) e en
’SELECT.depa men ’ could occu .
•When SUT e en ’SELECT.depa men ’ occu s, SUT
is now in s a e E; s a e Eis an e o s a e because he node
ha ep esen s i in Figu e 1has 2ci cles on i .
•(Pos -) Condi ion Q1: "depa men name ’YRI_ASSET’
is in able column ’depa men _name’ o da abase
able ’s ocks’"; applies in s a e E.
Thisshall no be he casesince depa men ’YRI_ASSET’
isnomo edefinedin SUT da abase able ’depa men ’.
5.2 "SDMM" WITH MORE THAN 2STATES
S a e Diag am Mealy Machines (SDMM) wi h mo e han 2
s a es ha e ollowing cha ac e is ics, as de ailed in scien ific and
enginee ing jou nal pape [Nou23] in p epa a ion:
•Only he fi s ansi ion has a p e-condi ion specifica ion
•Each o he ansi ion only has a pos -condi ion
specifica ion
•Since each s a e only has 1ou going s a e ansi ion, he
pos -condi ion o he p e ious (incoming) s a e ansi ion
ac s as he p e-condi ion o he nex ansi ion.
6 YERITH_QVGE (YRI_QVGE) Wo kflow
Figu e 10: Wo kflow explana ion.
use p ojec di ec o y:
"$USER_PROJECT_DIR/sd−mealy−machine−specs".
copy ".spec_sd_mealy" gene a ed
ile in o YRI−DB−RUNTIME−VERIF
YRI−DB−RUNTIME−VERIF
Ins umen SUT (sys em ude es )
wi h Q Dbus calls o
sa e y p ope y wi h
YRI_QVGE.
d aw SQL empo al
GENERATE A SINGLE
y i−db− un ime− e i execu able
"$YRI−DB−RUNTIME−VERIF".
using bash sc ip s in olde
The "Design and Tes ing Sys em" YERITH_QVGE wo ks wi h
ollowing wo kflow, as illus a ed g aphically in Figu e 10, and in
Figu e 5:
1. D aw S uc u e Que y Language (SQL) empo al sa e y
p ope y using d awing ool YERITH_QVGE;
2. copy he gene a ed ".spec_sd_mealy" files in o a use p ojec
di ec o y in YRI-DB-RUNTIME-VERIF home de elopmen
olde : "$YRI–DB–RUNTIME–VERIF";
3. ollow he s eps desc ibed in Sec ion 7so o ga he a single
execu able ha defines all specified un ime moni o s.
7 Cus om Use P ojec (YRI–DB–RUNTIME–VERIF)
Table 3: YRI-DB-RUNTIME-VERIF Di ec o ies
Va iable o illus a ion
pu poses
Meaning
$YRI–DB–RUNTIME–VERIF oo di ec o y o YRI-DB-
RUNTIME-VERIF
$YRI–DB–RUNTIME–VERIF/$USER_PROJECT oo di ec o y o use p ojec
Table 3illus a es di ec o ies ha will be used o desc ibe a
p ocess o gene a e a single bina y execu able o a use ’s cus om
p ojec wi h se e al un ime moni o specifica ions.
Figu e 7illus a es a sc eensho o he G aphical Use
In e ace (GUI) o YRI-DB-RUNTIME-VERIF. You can ge a copy o
YRI-DB-RUNTIME-VERIF using he ollowing command:
gi clone h ps://www.gi hub.com/ye i h d/y i-db- un ime- e i
C ea ing a bina y execu able o S a e Diag am Mealy
Machine (SDMM) specifica ions consis s o he ollowing
elemen s:
Au ho : Xa ie Noumbissi Noundou [P . P o . D .–Ing. ] Esp i –Sain . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "7 / 10". | Ve sion o – June 7, 2025 –
YERITH_QVGE use ’s guide YERITH &d
1. ’Ma iaDB’ da abase connec ion configu a ion file: his file
defines se ings o connec o he sys em unde es (SUT)
applica ion da abase; i is loca ed in pa h: "$YRI–DB–RUNTIME–
VERIF/YRI-DB-RUNTIME-VERIF-GUI-ELEMENTS-SETUP/y i-db- un ime-
e i -da abase-connec ion.p ope ies".
A da abase connec ion o he SUT applica ion da abase
is equi ed in o de o check LTL p ope y h ough he SDMM
applica ion lib a y YRI_SD_RUNTIME_VERIF_LANG.
2. P ope y configu a ion file: his file defines en i onmen
a iables necessa y o building a bina y execu able
o he use ; i is loca ed in pa h: "$YRI–DB–RUNTIME–
VERIF/$USER_PROJECT/bin/configu a ion-p ope ies.sh".
3. "$YRI–DB–RUNTIME–VERIF/$USER_PROJECT/sd-mealy-machine-specs":
his di ec o y con ains use defined S a e Diag am Mealy
Machine (SDMM) specifica ions o gene a e Co esponding
un ime moni o s wi hin a single bina y execu able.
4. Gene a e an execu able o a use defined un ime moni o :
a) A ollowing command MUST be enewed each ime you
a e new in a bash–shell en i onmen ; execu e ollowing
command in di ec o y "$YRI–DB–RUNTIME–VERIF":
. ./YRI-c ea e-execu able- o -use -SDMM.sh -d $USER_PROJECT
b) modi y he LTL e ifica ion code pa wi hin he gene a ed
sou ce code files.
Then execu e ollowing command in di ec o y "$YRI–DB–
RUNTIME–VERIF":
./y _db_ un ime_ e i _BUILD_DEBIAN_PACKAGE.sh
c) unins all YRI-DB-RUNTIME-VERIF wi h ollowing command
in di ec o y "$YRI–DB–RUNTIME–VERIF":
./y _DB_RUNTIME_VERIF_unins all.sh
d) e–ins all YRI-DB-RUNTIME-VERIF wi h ollowing command
in di ec o y "$YRI–DB–RUNTIME–VERIF":
./y _DB_RUNTIME_VERIF_INSTALL.SH
e) Redo [1s –s ep] in case you add o modi y a
’.spec_sd_mealy’ speci ica ion ile in olde "$YRI–DB–
RUNTIME–VERIF/$USER_PROJECT/sd-mealy-machine-specs" !
8 HOW TO START YRI-DB-RUNTIME-VERIF
•The "ELF-x64" bina y execu able, in he sou ce
de elopmen di ec o y is loca ed in ull pa h: "$YRI-
DB-RUNTIME-VERIF/bin".
•The DEBIAN–LINUX icon ( ) o YRI-DB-RUNTIME-
VERIF is loca ed in "Applica ions" menu unde sec ion
"P og amming", and sec ion "Accesso ies".
•The "ELF-x64" bina y execu able, a e ins alla ion o
he DEBIAN–LINUX package ’y i-db- un ime- e i .deb’ is
loca ed in ull pa h: "/op /y i-db- un ime- e i /bin".
Figu e 11: SAMPLE sql eco e y s a e diag am model in YERITH_QVGE
9 SQL QUERY Reco e y execu ion on demand
A use can speci y which SQL command que y o execu e
whene e a Sys em Unde Tes (SUT) lands in an accep ing e o
s a e. This is done using keywo ds ending wi h "AUTO", used o
meaning "AUTO RECOVERY FROM FAIL STATE":
1. eco e y_sql_que y
2. END_STATE_AUTO
3. FINAL_STATE_AUTO
4. ERROR_STATE_AUTO.
The use o an "AUTO" keywo d shall be accompanied wi h
a use o keywo d eco e y_sql_que y, ha specifies a SQL
command que y o un when landing in his ail e o accep ing
s a e.
9.1 Au oma ic SQL Command Que y Gene a ion
YERITH_QVGE implemen s an au oma ic SQL que y gene a ion
s a egy incasea use don’ speci y aSQLcommand que y, sincei
could be lea ed emp y: Subsec ions 9.1.1,9.1.2,9.1.3, and 9.1.4
desc ibe he s a egy implemen ed.
Au ho : Xa ie Noumbissi Noundou [P . P o . D .–Ing. ] Esp i –Sain . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "8 / 10". | Ve sion o – June 7, 2025 –
YERITH_QVGE use ’s guide YERITH &d
9.1.1 ERROR ACCEPTING STATE o sdmm 1.
no in_be o e (YX,YY)ACTION (V)
in_a e (DD,YR)
9.1.2 RECOVERY 1.
in_a e (DD,YR)ACTION (RECOVERY_ND)
no in_a e (DD,YR)
9.1.3 RECOVERY 2 (P ac ical solu ion o be implemen ed in
YRI-DB-RUNTIME-VERIF.
in_a e (DD,YR)ACTION (RECOVERY_D)
in_a e (YX,YY)
9.1.4 Conc e e RECOVERY 2 ac ion.
in_a e (YX,YY)inse _RECOVERY (YX,YY)
in_be o e (YX,YY)•
10 HOW TO USE a use in e ace
Figu e 12: YERITH_QVGE use in e ace sc eensho .
11 YRI_SD_RUNTIME_VERIF SPECIFICATION LANGUAGE
Figu e 13 illus a es a ”Backus-NAUR o m (BNF)” o ou specifica ion language o YRI-DB-RUNTIME-VERIF ool.
12 Fo mal Scien ific and Enginee ing P ojec Desc ip ion
De ailed o mal scien ific and enginee ing con ibu ions o design
and es ing sys em YERITH_QVGE can be ound in JOURNAL
ARTICLE "Run ime Ve i ica ion O SQL Co ec ness P ope ies
wi h YRI-DB-RUNTIME-VERIF" [Nou23].
13 Conclusion
The g aphical d awing ool YERITH_QVGE (Figu e 6) cos s only
2, 500 EUROS. WE ONLY SUPPORT DEBIAN–LINUX (h ps:
//www.debian.o g).
Re e ences
[Nou23] Xa ie Noundou. A F amewo k o Ve i ying SQL
Co ec ness Tempo al P ope ies o [GUI] So wa e
a Run ime. h ps://zenodo.o g/ eco ds/
13232567, Oc obe 2023.
Au ho : Xa ie Noumbissi Noundou [P . P o . D .–Ing. ] Esp i –Sain . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "9 / 10". | Ve sion o – June 7, 2025 –
YERITH_QVGE use ’s guide YERITH &d
Figu e 13: G amma in Backus–Nau Fo m (BNF) o YRI_SD_RUNTIME_VERIF_LANG Mealy Machine STATE DIAGRAM Specifica ion
Language.
〈speci ica ion〉::= y i_sd_mealy_au oma on_spec ’{’ 〈mealy-au oma on-spec〉’.’ ’}’
〈mealy-au oma on-spec〉::= 〈su -s a e-spec〉
|〈su -s a e-spec〉’→’〈su -edge-s a e-spec〉
〈su -edge-s a e-spec〉::= 〈su -edge-mealy-au oma on-spec〉’→’〈mealy-au oma on-spec〉
〈su -edge-mealy-au oma on-spec〉::= 〈edge-mealy-au oma on-gua d-cond〉 〈e en -call〉
〈edge-mealy-au oma on-gua d-cond〉::= /* emp y */ ’/’ | ’[’ 〈 ace-speci ica ion〉’]’ ’/’
〈 ace-speci ica ion〉::= 〈in-sql-e en -log〉|〈no -in-sql-e en -log〉|〈in-se - ace〉|〈no -in-se - ace〉
〈su -s a e-spec〉::= 〈s a -s a e-p ope y-spec〉
|〈s a -s a e-p ope y-spec〉’:’ 〈algeb a-se -speci ica ion〉
|〈s a e-p ope y-spec〉’:’ 〈algeb a-se -speci ica ion〉
|〈 inal-s a e-p ope y-spec〉’:’ 〈algeb a-se -speci ica ion〉
|〈 inal-s a e-au o-p ope y-spec〉’:’ 〈algeb a-se -speci ica ion〉’:’ 〈 eco e y-sql-que y-spec〉
〈algeb a-se -speci ica ion〉::= 〈in-algeb a-se -spec〉|〈no -in-algeb a-se -spec〉
〈in-algeb a-se -spec〉::= 〈in-spec〉’(’ 〈p og- a iable〉’,’ 〈db- able〉’.’ 〈db-column〉’)’
|〈in-spec-nop〉’(’ ’)’
〈no -in-algeb a-se -spec〉::= 〈no -in-spec〉’(’ 〈p og- a iable〉’,’ 〈db- able〉’.’ 〈db-column〉’)’
|〈no -in-spec-nop〉’(’ ’)’
〈in-sql-e en -log〉::= in_sql_e en _log’(’ 〈e en -call〉’,’ 〈s a e-p ope y-speci ica ion〉’)’
〈no -in-sql-e en -log〉::= no _in_sql_e en _log’(’ 〈e en -call〉’,’ 〈s a e-p ope y-speci ica ion〉’)’
〈in-se - ace〉::= in_se _ ace’(’ 〈e en -call〉’,’ 〈s a e-p ope y-speci ica ion〉’)’
〈no -in-se - ace〉::= no _in_se _ ace’(’ 〈e en -call〉’,’ 〈s a e-p ope y-speci ica ion〉’)’
〈in-spec〉::= IN_BEFORE |IN_AFTER |IN_PRE |IN_POST
〈in-spec-nop〉::= IN_POST_NOP
〈no -in-spec〉::= NOT_IN_BEFORE |NOT_IN_AFTER |NOT_IN_PRE |NOT_IN_POST
〈no -in-spec-nop〉::= NOT_IN_POST_NOP
〈s a -s a e-p ope y-spec〉::= START_STATE’(’ AlphaNum ’)’
〈s a e-p ope y-spec〉::= STATE’(’ AlphaNum ’)’
〈 inal-s a e-p ope y-spec〉::= END_STATE’(’ AlphaNum ’)’ | FINAL_STATE’(’ AlphaNum ’)’ | ERROR_STATE’(’ AlphaNum ’)’
〈 inal-s a e-au o-p ope y-spec〉::= END_STATE_AUTO’(’ AlphaNum ’)’ | FINAL_STATE_AUTO’(’ AlphaNum ’)’
|ERROR_STATE_AUTO’(’ AlphaNum ’)’
〈 eco e y-sql-que y-spec〉::= eco e y_sql_que y’(’ 〈db- able〉’,’ 〈sql- eco e y-que y〉’)’
〈sql- eco e y-que y〉::= S ing
〈e en -call〉::= S ing
〈p og- a iable〉::= AlphaNum
〈db- able〉::= AlphaNum
〈db-column〉::= AlphaNum
Au ho : Xa ie Noumbissi Noundou [P . P o . D .–Ing. ] Esp i –Sain . YERITH–NISSI. (JEOVAH–NISSI IN HEAVEN.) Page "10 / 10". | Ve sion o – June 7, 2025 –
