Determination of Formal Methods Capabilities for Software Specification and Analysis
Subject Areas : electrical and computer engineeringAbstract :
Software developers face the problem of adopting a suitable formal method to developing their software. We aim to determine capability level of formal methods in software specification and analysis in four steps. The first step introduces the criteria by which the formal methods assess. The second and third ones deal with categorizing sorts of software and formal methods based on their solution methods. The fourth step determines fitness of some typical formal methods to specification and analysis of each software category.
References:
[1] E. M. Clarke and J. M. Wing, "Formal methods: state of the art and future directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, Dec. 1996.
[2] C. Heitmeyer, "On the need for practical formal methods," in Formal Techniques in Real Time and Real - Time Fault - Tolerant Systems, Proc. of the 5th Intern. Symposium, Springer, pp. 18-26, 1998.
[3] H. Oberheid, "A coloured Petri - Net model of cooperative arrival planning in air traffic control," in K. Jensen (Ed.): Proc. of the 17th Worskhop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, pp. 177-196, 2006.
[4] C. Heitmeyer, M. Archer, R. Bharadwaj, and R. Jeffords, "Tools for constructing requirements specifications, the SCR toolset at the age of ten," Int. J. of Comput. Syst. Sci. & Eng., vol. 1, pp. 19-35, 2005.
[5] B. Berard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux, "Comparison of the expressiveness of timed automata and time Petri Nets," in Proc. of 3rd Int. Conf. on Formal Modeling and Analysis of Timed Systems, vol. 3829, pp. 211-225, 2005.
[6] H. Habrias and M. Frrapier, "Software specification methods, an overview using a case study," Book Chapter in Formal Approach to Computing and Information Technology, pp. 11-20, 2006.
[7] I. V. Weerd, S. Weerd, and S. Brinkkemper, "Developing a reference method for game production by method comparison," in Proc. of IFIP Int. Federation for Information Processing, Spring, vol. 244, pp. 327-313, 2007.
[8] X. Hei, L. Chang, W. Ma, J. Gao, and G. Xie, "Automatic transformation from UML Statechart to Petri Nets for safety analysis and verification," in Proc. of Int Conf. on Quality, Reliability, Risk, Maintenance, and Safety Engineering, pp. 948-951, 2011.
[9] A. M. K. Cheng, Real - Time Systems: Scheduling, Analysis, and Verification, Wiley, 2002.
[10] R. M. Amadio and D. Lugiez (Eds), Concurrency Theory, Springer, 2003.
[11] G. Sukumar, Distributed Systems - an Algorithmic Approach, Chapman & Hall/CRC, 2007.
[12] I. Fogg, B. Hicks, A. Lister, T. Mansfield, and K. Reymond, "A comparison of Lotos and Z for specifying distributed systems," Australian Computer Science Communications, vol. 12, no. 1, pp. 88-96, Feb. 1990.
[13] R. Stuart and P. Norvig, Artificial Intelligence: a Modern Approach, 3rd Ed., Prentice Hall, 2010.
[14] K. Munn and B. Smith, Applied Ontology: an Introduction, Ontos Verlag, 2008.
[15] M. Jarrar and R. Meersman, "Ontology engineering - the DOGMA approach," Advances in Web Semantics I, LNCS, vol. 4891, pp. 7-34, Springer. 2008.
[16] B. Smith et al, "The OBO foundry: coordinated evolution of ontologies to support biomedical data integration," Journal of Nature Biotechnology, vol. 25, no. 11, pp. 1251-1255, 2007.
[17] P. McCorduck, Machines Who Think, 2nd Ed., A K Peters/CRC Press, 2004.
[18] I. Brakto, Prolog Programming for Artificial Intelligence, Addison Wesley, 2001.
[19] J. C. Giarratano and R. Gary, Expert Systems, Principles and Programming, Thomson Course Technolog, 2005.
[20] L. A. Zadeh, "Fuzzy sets," Information and Control, vol. 8, no. 3, pp. 338-353, 1965.
[21] P. J. Haas, "Stochastic Petri Nets: modeling, stability, simulation," Springer, 2002.
[22] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel - Schneider, The Description Logic Handbook, Cambridge University Press, 2007.
[23] S. M. Brien, "The development of Z., In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors, Semantics of Specification Languages (SoSL), Workshops in Computing, pp. 1-14, Springer, 1994.
[24] J. P. Bowen, Formal Specification and Documentation Using Z: A Case Study Approach, International Thomson Computer Press, pp. 1-65, 2003.
[25] S. Stepney, R. Barden, and D. Cooper (Eds.), "Object orientation in Z," Workshops in Computing, Springer, 1992.
[26] http://czt.sourceforge.net/index.html
[27] J. R. Abrial, Modeling in Event - B: System and Software Engineering, Cambridge University Press, 2010.
[28] http://www.event-b.org/platform.html
[29] F. Jahanian and A. Mok, "Modechart: a specification language for real - time systems," IEEE Trans. on Software Engineering, vol. 20, no. 12, pp. 933-947, Dec. 1994.
[30] D. A. Stuart, "Implementing a verifier for real - time systems," in Proc. of IEEE Real - Time Systems Symposium, pp. 62-71, 1990.
[31] A. E. Abdallah, C. B. Jones, and J. W. Sanders (Eds.), "Communicating sequential processes, the first 25 years," Lecture Notes in Computer Science, vol. 3525, 2005.
[32] J. Carter and W. B. Gardner, "A formal CSP framework for message - passing HPC programming," in Proc. of Canadian Conf. on Electrical and Computer Engineering, pp. 1466-1470, 2006.
[33] S. Jun, Y. Liu, and J. Song Dong, "Model checking CSP revisited: introducing a process analysis toolkit," in Proc. of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, Springer, pp. 307-322, 2008.
[1] E. M. Clarke and J. M. Wing, "Formal methods: state of the art and future directions," ACM Computing Surveys, vol. 28, no. 4, pp. 626-643, Dec. 1996.
[2] C. Heitmeyer, "On the need for practical formal methods," in Formal Techniques in Real Time and Real - Time Fault - Tolerant Systems, Proc. of the 5th Intern. Symposium, Springer, pp. 18-26, 1998.
[3] H. Oberheid, "A coloured Petri - Net model of cooperative arrival planning in air traffic control," in K. Jensen (Ed.): Proc. of the 17th Worskhop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, pp. 177-196, 2006.
[4] C. Heitmeyer, M. Archer, R. Bharadwaj, and R. Jeffords, "Tools for constructing requirements specifications, the SCR toolset at the age of ten," Int. J. of Comput. Syst. Sci. & Eng., vol. 1, pp. 19-35, 2005.
[5] B. Berard, F. Cassez, S. Haddad, D. Lime, and O. H. Roux, "Comparison of the expressiveness of timed automata and time Petri Nets," in Proc. of 3rd Int. Conf. on Formal Modeling and Analysis of Timed Systems, vol. 3829, pp. 211-225, 2005.
[6] H. Habrias and M. Frrapier, "Software specification methods, an overview using a case study," Book Chapter in Formal Approach to Computing and Information Technology, pp. 11-20, 2006.
[7] I. V. Weerd, S. Weerd, and S. Brinkkemper, "Developing a reference method for game production by method comparison," in Proc. of IFIP Int. Federation for Information Processing, Spring, vol. 244, pp. 327-313, 2007.
[8] X. Hei, L. Chang, W. Ma, J. Gao, and G. Xie, "Automatic transformation from UML Statechart to Petri Nets for safety analysis and verification," in Proc. of Int Conf. on Quality, Reliability, Risk, Maintenance, and Safety Engineering, pp. 948-951, 2011.
[9] A. M. K. Cheng, Real - Time Systems: Scheduling, Analysis, and Verification, Wiley, 2002.
[10] R. M. Amadio and D. Lugiez (Eds), Concurrency Theory, Springer, 2003.
[11] G. Sukumar, Distributed Systems - an Algorithmic Approach, Chapman & Hall/CRC, 2007.
[12] I. Fogg, B. Hicks, A. Lister, T. Mansfield, and K. Reymond, "A comparison of Lotos and Z for specifying distributed systems," Australian Computer Science Communications, vol. 12, no. 1, pp. 88-96, Feb. 1990.
[13] R. Stuart and P. Norvig, Artificial Intelligence: a Modern Approach, 3rd Ed., Prentice Hall, 2010.
[14] K. Munn and B. Smith, Applied Ontology: an Introduction, Ontos Verlag, 2008.
[15] M. Jarrar and R. Meersman, "Ontology engineering - the DOGMA approach," Advances in Web Semantics I, LNCS, vol. 4891, pp. 7-34, Springer. 2008.
[16] B. Smith et al, "The OBO foundry: coordinated evolution of ontologies to support biomedical data integration," Journal of Nature Biotechnology, vol. 25, no. 11, pp. 1251-1255, 2007.
[17] P. McCorduck, Machines Who Think, 2nd Ed., A K Peters/CRC Press, 2004.
[18] I. Brakto, Prolog Programming for Artificial Intelligence, Addison Wesley, 2001.
[19] J. C. Giarratano and R. Gary, Expert Systems, Principles and Programming, Thomson Course Technolog, 2005.
[20] L. A. Zadeh, "Fuzzy sets," Information and Control, vol. 8, no. 3, pp. 338-353, 1965.
[21] P. J. Haas, "Stochastic Petri Nets: modeling, stability, simulation," Springer, 2002.
[22] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel - Schneider, The Description Logic Handbook, Cambridge University Press, 2007.
[23] S. M. Brien, "The development of Z., In D. J. Andrews, J. F. Groote, and C. A. Middelburg, editors, Semantics of Specification Languages (SoSL), Workshops in Computing, pp. 1-14, Springer, 1994.
[24] J. P. Bowen, Formal Specification and Documentation Using Z: A Case Study Approach, International Thomson Computer Press, pp. 1-65, 2003.
[25] S. Stepney, R. Barden, and D. Cooper (Eds.), "Object orientation in Z," Workshops in Computing, Springer, 1992.
[26] http://czt.sourceforge.net/index.html
[27] J. R. Abrial, Modeling in Event - B: System and Software Engineering, Cambridge University Press, 2010.
[28] http://www.event-b.org/platform.html
[29] F. Jahanian and A. Mok, "Modechart: a specification language for real - time systems," IEEE Trans. on Software Engineering, vol. 20, no. 12, pp. 933-947, Dec. 1994.
[30] D. A. Stuart, "Implementing a verifier for real - time systems," in Proc. of IEEE Real - Time Systems Symposium, pp. 62-71, 1990.
[31] A. E. Abdallah, C. B. Jones, and J. W. Sanders (Eds.), "Communicating sequential processes, the first 25 years," Lecture Notes in Computer Science, vol. 3525, 2005.
[32] J. Carter and W. B. Gardner, "A formal CSP framework for message - passing HPC programming," in Proc. of Canadian Conf. on Electrical and Computer Engineering, pp. 1466-1470, 2006.
[33] S. Jun, Y. Liu, and J. Song Dong, "Model checking CSP revisited: introducing a process analysis toolkit," in Proc. of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation, Springer, pp. 307-322, 2008.