Requirement Formalization for Model Checking using Extended Backus Naur Form

E. O. Aliyu*, O. S. Adewale**, A. O. Adetunmbi***, B. A. Ojokoh****
*Department of Computer Science, Adekunle Ajasin University, Akungba Akoko, Nigeria.
**-****Department of Computer Science, Federal University of Technology Akure, Nigeria.
Periodicity:January - March'2019


Describing the structure of a language using rewriting rules in verifying requirements and design is still a vivid area of research. We 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 a 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.


Requirement Formalization, Model Checking, BNF, EBNF, Syntax.

How to Cite this Article?

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), 26-31.


Purchase Instant Access

Single Article

North Americas,UK,
Middle East,Europe
India Rest of world
Pdf 35 35 200 20
Online 35 35 200 15
Pdf & Online 35 35 400 25

If you have access to this article please login to view the article or kindly login to purchase the article
Options for accessing this content:
  • If you would like institutional access to this content, please recommend the title to your librarian.
    Library Recommendation Form
  • If you already have i-manager's user account: Login above and proceed to purchase the article.
  • New Users: Please register, then proceed to purchase the article.