DEVELOPMENT OF MODEL CHECKING TECHNIQUE FOR OPERATORS CONFORMITY ERROR IN SELECTIVE AND ITERATIVE STRUCTURES

Abstract

Software model checking checks the properties of models of program under consideration. The major goal of software model checker is to ensure system correctness and eliminate bugs from such systems. This research proposed model checking technique for operator’s conformity error such as assignment in-guard error in selective and iterative structures based on abstract interpretation. The proposed system is divided into five (5) phases. In phase I, code instrumentation takes place at the lexer/parsing phase to analyse the code under consideration. The lexer was based on regular expression python compiler versions 3 library for matching text into a stream of tokens. Extended Backus Naur Form (EBNF) was employed to formally specify the system to check, transform into program using Recursive Descent parsing technique and Best First Search (BFS) algorithm was used in the parser development to explore the grammar and obtain a required string. In phase II, determining the structure of the string relative to the grammar was handled by Graph Visualisation Software (Graphiz), which parsed the string into a dot file and converted the dot file into Portable Network Graphic (PNG) format called Abstract Syntax Tree (AST). In phase III, AST, an instance of program model encodes the programming language construct while the children of each node represent component of the construct. In phase IV, AST, an instance of specification model encodes the properties a system must satisfy based on Predicate Abstraction (PA). In phase V, AST, an instance of a model checker used the principle of conformity checks and conformity rule based on IF-THEN rule to determine the satisfaction or refutation of the properties checked against the model. The proposed model was implemented using python compiler version 3, window operating system, Graphiz tool and text editor (Ms word) while Intel (R) core TM i3-5005u 2.00GHz, 4.00GB of RAM and 100MB hard disk are the hardware requirement specification the computer system used. The proposed system performance was evaluated using date command by means of a simple if else statement line of codes (LOC) of 100, 500, 2000, 5000, 20000 and 50000 respectively over 10 runs for Intel core i3-5005u 2.00GHz with 4.00GB, AMD E1-1200APU 1.40GHz with 4.00GB and Intel core i7-3632qm 2.20GHz with 8.00GB to determine if the program is optimal or not and further deduce a mathematical model for calculating the scheduled time for different program LOC. Time performance measure of each control structures into 1000 LOC was carried out, where ‘for’ statement have an edge in the iterative area while ‘switch’ and ‘if ’ statements performed relatively the same in the case of conditional argument. Finally, time performance tests between the model checker, the program model and specification model were examined. Model checker performance measure 33.77%, program model measure 33.00% and specification model is 33.23%. The result shows that program model execute faster. The model checker was tested for reliability and validity by showing their effectiveness on C++ programs for operator’s conformity error within program statements.