Requirement Formalization for Model Checking using Extended Backus Naur Form

Volume 13 Issue 3 January - March 2019

Research Paper

Requirement Formalization for Model Checking using Extended Backus Naur Form

E. O. Aliyu*, O. S. Adewale**, A. O. Adetunmbi***, B. A. Ojokoh****

* Lecturer, Department of Computer Science, Adekunle Ajasin University, Akungba Akoko, Nigeria.

** Dean and Professor, Department of Computer Science, Federal University of Technology Akure, Nigeria.

*** Professor, Department of Computer Science, Federal University of Technology Akure, Nigeria.

**** Associate Professor, Department of Computer Science, Federal University of Technology Akure, Nigeria.

Aliyu, E. O., Adewale, O. S., Adetunmbi, A. O., Ojokoh, B. A. (2019). Requirement Formalization for Model Checking using Extended Backus Naur Form, i-manager's Journal on Software Engineering, 13(3), 1-6. https://doi.org/10.26634/jse.13.3.15687

Abstract

Describing the structure of a language using rewriting rules in verifying requirements and design is still a vivid area of research. The authors describe the grammar formalism Extended Backus Naur Form (EBNF) to specify the 'if' single block construct with respect to assignment and relational operators as well as Switch, For loop, Do-while, and While loop statement to ensure program free flow. This aim to ensure correctness in the grammar rule for selective and iterative construct to parse C++ programs. The grammar describes the actions a parser must take to parse a string of tokens correctly.