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.
Periodicity:January - March'2019
DOI : 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.

Keywords

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), 1-6. https://doi.org/10.26634/jse.13.3.15687

References

[1]. Adetunmbi, A. O. (2012). Theory of computation (Lecture notes), Federal University of Technology Akure, Ondo State, Nigeria.
[2]. Adewale, O. S. (2010). Compiler construction, (Lecture notes), Federal University of Technology Akure, Ondo State, Nigeria.
[3]. Aggarwal, K. K., & Yogesh S. (2008). Software Engineering (Third Edition), Delhi: New Age.
[4]. Baudin, P., Filliatre, J. C., Marche, C., Monate, B., Moy, Y., & Prevosto, V. (2008). ACSL : ANSI / ISO C specification language, CAT RNTL Project, INRIA.
[5]. Berard, B. M., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petnicci, L., & Schnoebelen, P. (2001). System and software verification. Model checking techniques and tools. Springer- Verlag Berlin Heidelberg, Retrieved from https://www.springer.com/in/book/9783540415237
[6]. Biere, A. (2008). Tutorial on model checking: Modelling and verification in computer science. In International Conference on Algebraic Biology (pp. 16-21). Springer, Berlin, Heidelberg.
[7]. Emani, C., Silva, C. F. D., Fiès, B., Zarli, A., & Ghodous, P. (2016, October). An Approach for Automatic Formalization of Business Rules. In Proc. of the 33rd CIB W78 Conference 2016.
[8]. Espada, M. A. V. (2005). Modal abstraction and replication of processes with data (Doctoral dissertation), University of Amsterdam.
[9]. Forsberg, M., & Ranta, A. (2005). The labelled BNF grammar formalism. Department of Computing Science, Chalmers University of Technology and the University of Gothenburg, Sweden.
[10]. Gabbrielli, M., & Martini, S. (2010). Programming languages: principles and paradigms, London: Springer.
[11]. Kammer, D., Wojdziak, J., Keck, M., Groh, R., & Taranko, S. (2010, November). Towards a formalization of multi-touch gestures. In ACM International Conference on Interactive Tabletops and Surfaces (pp. 49-58). ACM.
[12]. Laros, J. F., Blavier, A., Dunnen, J. T. D., & Taschner, P. E. (2011). A formalized description of the standard human variant nomenclature in Extended Backus-Naur Form. BMC Bioinformatics, 12(4), S5.
[13]. Louden, K. C., & Adams, P. (1993). Programming Languages: Principles and Practice, Belmont, CA: Wadsworth
[14]. Mann, P. B. (2006). A translational BNF grammar notation (TBNF). ACM SIGPLAN Notices, 41(4), 16-23.
[15]. Overbey, J. L., & Johnson, R. E. (2008, September). Generating rewritable abstract syntax trees. In International Conference on Software Language Engineering (pp. 114- 133). Heidelberg: Springer, Berlin.
[16]. Park, S., Lee, Y. C., & Lee, J. K. (2016). Definition of a domain-specific language for Korean building act sentences as an explicit computable form. Journal of Information Technology in Construction (ITcon), 21(26), 422-433.
[17]. Scowen, R. S. (1998). Extended BNF-a generic base standard. (Draft Papers). Retrieved from http://www.cl.cam.ac.uk/mgk25/iso-14977.Pdf
[18]. Shehitoglu, O. T. (2009). Programming languages: syntax description and parsing. [Power point presentation] Retrieved from http://ocw.metu.edu.tr/pluginfile.php/ 2987/mod_resource/content/0/lectures/15-syntax-parsing. pdf
[19]. Xah, L. (2014). What's the difference between BNF, EBNF, ABNF. Retrieved from http://xahlee.info/ parser/bnf_ebnf_abnf.html
If you have access to this article please login to view the article or kindly login to purchase the article

Purchase Instant Access

Single Article

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

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.