We apologize for a recent technical issue with our email system, which temporarily affected account activations. Accounts have now been activated. Authors may proceed with paper submissions. PhDFocusTM
CFP last date
20 November 2024
Reseach Article

Formal Methods in Requirements Phase of SDLC

by S. K. Pandey, Mona Batra
International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 70 - Number 13
Year of Publication: 2013
Authors: S. K. Pandey, Mona Batra
10.5120/12020-8017

S. K. Pandey, Mona Batra . Formal Methods in Requirements Phase of SDLC. International Journal of Computer Applications. 70, 13 ( May 2013), 7-14. DOI=10.5120/12020-8017

@article{ 10.5120/12020-8017,
author = { S. K. Pandey, Mona Batra },
title = { Formal Methods in Requirements Phase of SDLC },
journal = { International Journal of Computer Applications },
issue_date = { May 2013 },
volume = { 70 },
number = { 13 },
month = { May },
year = { 2013 },
issn = { 0975-8887 },
pages = { 7-14 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume70/number13/12020-8017/ },
doi = { 10.5120/12020-8017 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T21:32:44.745974+05:30
%A S. K. Pandey
%A Mona Batra
%T Formal Methods in Requirements Phase of SDLC
%J International Journal of Computer Applications
%@ 0975-8887
%V 70
%N 13
%P 7-14
%D 2013
%I Foundation of Computer Science (FCS), NY, USA
Abstract

Currently, there is an increasing demand for more rigorous and systematic approaches to develop security critical software systems across the globe. The complexity of the software system is rapidly raising due to the inclusion of properties like security and reliability. The process of software development complicates with the raising complexity of the software system. As a result, formal methods are currently used to model complex security critical systems. Literature reveals that formal methods can be applied at various points through the development process. Their tools can provide automated support, needed for checking completeness, traceability, verifiability, reusability and inconsistency management of requirement specification, which is the backbone of entire SDLC. Accordingly, there appears a need for a critical review of these formal methods. The paper presents a brief discussion on various formal methods particularly Z-method, B-method, VDM, OBJ, Larch and Communicating Sequential Process etc. along with their strengths and weaknesses followed by a comparative study on the basis of the review results. The present research work may help the software developers to provide their recommendations for using formal methods at different stages of software development and particularly for requirements phase, based on the specific requirements of an organization.

References
  1. M. Clarke Edmund, M. Wing Jeannette: Formal Methods: State of the Art and Future Directions, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA. Retrieved on April, 8, 2013. http://www. site. uottawa. ca/~bochmann/ELG7187C/CourseNotes/Literature/Clarke%20%20FM%20State%20of%20the%20art%20-%2096. pdf
  2. Fuxman Ariel Damian: Formal Analysis of Early Requirements Specifications, Graduate Department of Computer Science, University of Toronto, 2001. Retrieved on April, 8, 2013 http://wenku. baidu. com/view/806eb2b8fd0a79563c1e72b5. html
  3. Woodcock Jim, Larsen Peter Gorm, Bicarregui Juan and Fitzgerald John: Formal Methods: Practice and Experience, ACM Computing Surveys( CSUR), Volume 41 Issue 4, October 2009 Article No. 19. Retrieved on: March 17, 2013. http://deployeprints. ecs. soton. ac. uk/161/2/fmsurvey%5B1%5D. pdf
  4. Pressman Roger S. : "Software Engineering"- A Practitioner's Approach", McGraw Hill, 5th edition. 2000.
  5. Ogilvie Paul: Formal Methods in Requirements Engineering. Retrieved on: March, 17,2013 http://www. google. co. in/url?sa=t&rct=j&q=paul%20ogilvie%20formal%20methods%20in%20requirement%20engineering&source=web&cd=1&cad=rja&ved=0CC4QFjAA&url=http%3A%2F%2Fciteseerx. ist. psu. edu%2Fviewdoc%2Fdownload%3Fdoi%3D10. 1. 1. 93. 8000%26rep%3Drep1%26type%3Dpdf&ei=ispFUeXGBNCzrAfP6oHgDQ&usg=AFQjCNHuCyMppgBZ5cxA0QAOhfOIYZL8Lw&bvm=bv. 43828540,d. bmk
  6. Kaur Arvinder, Gulati Samridhi and Singh Sarita: Analysis of Three Formal Methods-Z, B and VDM, International Journal of Engineering Research & Technology (IJERT) Vol. 1 Issue 4, June – 2012. Retrieved on April, 8,2013. https://www. google. co. in/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDMQFjAA&url=http%3A%2F%2Fwww. ijert. org%2Fbrowse%2Fjune-2012 edition%3Fdownload%3D297%253Aanalysis-of-three-formal-methods-z-b-and-vdm%26start%3D120&ei=4
  7. McGibbon Thomas: An Analysis of Two Formal Methods: VDM and Z, ITT Industries - Systems Division.
  8. Muller Andreas: VDM: The Vienna Development Method, April 20, 2009. Retrieved on April, 7, 2013. https://www. google. co. in/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&ved=0CDMQFjAA&url=http%3A%2F%2Fciteseerx. ist. psu. edu%2Fviewdoc%2Fdownload%3Fdoi%3D10. 1. 1. 153. 3064%26rep%3Drep1%26type%3Dpdf&ei=FXNlUen9DobqrAfgroCwAg&usg=AFQjCNGYrKJJCI1xnt3tvME2JQFyDe1jaQ&sig2=LpGghBpScvnLXpXuxMxXyQ&bvm=bv. 44990110,d. bmk
  9. Spivey J. M. : The Z Notation: A Reference Manual. 2nd Edition, New York,Prentice-Hall, (1998). Retrieved on March, 19, 2013 http://www. google. co. in/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&cad=rja&sqi=2&ved=0CDgQFjAB&url=http%3A%2F%2Ftrac. assembla. com%2Fci4712%2Fexport%2F54%2FZReferenceManual. pdf&ei=kDNIUfPJNsW8rAfl94CgCw&usg=AFQjCNEsUr2UIEtvntbzhFR9LoVWzGC6Rw&sig2=CrXzdXFsi5PvCc5FQgHR4w&bvm=bv. 43828540,d. bmk
  10. B method - An overview through example Ewa Romanowicz, McMaster University, Hamilton, Ontario, Canada April 17, 2008. Retrieved on April, 6, 2013. http://www. ewaromanowicz. com/academics/B_method_An_overview_through_example. pdf
  11. Delgado Antonio Ruiz, Pitt David and Smythe Colin: A Review of Object Oriented Approaches in Formal Methods, The Computer Journal, Vol. 38, NO 10, 1995.
  12. Pedersen Jan Storbank and Klein Mark H. : Using the Vienna Development Method (VDM) To Formalize a Communication Protocol, Technical Report, November 1988. Retrieved on April, 6, 2013. ftp://ftp. sei. cmu. edu/pub/documents/88. reports/pdf/tr26. 88. pdf
  13. Schneider S. : The B-Method: An Introduction. Cornerstones of Computing, Palgrave, 2001. Retrieved on April, 5,2013. http://www. amazon. com/B-Method-Cornerstones-Computing-Steve-Schneider/dp/033379284X
  14. Bjorner Dines and C. Henson Martin: Logics of Specification Languages. Springer Berlin Heidelberg, 2007.
  15. Wikipedia. OBJ. Retrieved on March 18, 2013. From http://en. wikipedia. org/wiki/OBJ_(programming_language)
  16. Guttag J. V. , Horning J. J. , Garland S. J. , Jones K. D. , Modet A. , and Wing J. M. : Larch: Languages and Tools for Formal Speci?cation, January 1993. Retrieved on April 10, 2013. http://www. cs. cmu. edu/afs/cs/usr/wing/www/publications/LarchBook. pdf
  17. Dunstan Martin, Kelsey Tom, Linton Steve and MartinL Ursula: Lightweight Formal Methods For Computer Algebra Systems, University of St Andrews, UK Retrieved on April 10, 2013 http://www. eecs. qmul. ac. uk/~uhmm/papers/AdGotMar. pdf
  18. Cheng, Betty H C, Atlee, Joanne M: Research Directions in Requirements Engineering, IEEE, May 2007, pp 285 – 303.
Index Terms

Computer Science
Information Sciences

Keywords

Formal Methods Comparative Study of Formal Methods Requirements Engineering Z-method B-method VDM OBJ Larch Communicating Sequential Process