Extending Operation Semantics to Enhance the Applicability of Formal Refinement

  • Shaoying Liu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


This paper proposes an extension of operation semantics and discusses its benefits in enhancing the applicability of Morgan’s formal refinement calculus in practical software development.


Formal Method Partial Relation Correct Program Restricted Domain Composite Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall (1994)Google Scholar
  2. 2.
    Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall (1996)Google Scholar
  3. 3.
    Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996)Google Scholar
  4. 4.
    Leuschel, M., Butler, M.: Automatic Refinement Checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 345–359. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Boiten, E.A.: Loose specification and refinement in Z. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 226–241. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Liu, S., Shibata, M., Sat, R.: Applying SOFL to Develop a University Information System. In: Proceedings of 1999 Asia-Pacific Software Engineering Conference (APSEC 1999), Takamatsu, Japan, pp. 404–411. IEEE Computer Society Press (1999)Google Scholar
  7. 7.
    Hall, A.: Seven Myths of Formal Methods. IEEE Software, 11–19 (1990)Google Scholar
  8. 8.
    Liu, S.: A Case Study of Modeling an ATM Using SOFL. Technical Report HCIS-2003-01, CIS, Hosei University, Koganei-shi, Tokyo, Japan (2003)Google Scholar
  9. 9.
    Smith, G.: The Object-Z Specification Language. In: Advances in Formal Methods. Kluwer Academic (2000)Google Scholar
  10. 10.
    Utting, M.: An Object-Oriented Refinement Calculus with Modular Reasoning. PhD thesis, University of New South Wales, Australia (1992)Google Scholar
  11. 11.
    Cavalcanti, A., Naumann, D.A.: Forward Simulation for Data Refinement of Classes. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 471–490. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Hall, A.: Realising the Benefits of Formal Methods. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 1–4. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Liu, S., Asuka, M., Komaya, K., Nakamura, Y.: An Approach to Specifying and Verifying Safety-Critical Systems with Practical Formal Method SOFL. In: Proceedings of the Fourth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 1998), Monterey, California, USA, pp. 100–114. IEEE Computer Society Press (1998)Google Scholar
  14. 14.
    Parnas, D.L., Weiss, D.M.: Active Design Reviews: Principles and Practices. Journal of Systems and Software 7, 259–265 (1987)CrossRefGoogle Scholar
  15. 15.
    Heitmeyer, C.L., Bull, A., Gasarch, C., Labaw, B.: SCR*: A Toolset for Specifying and Analyzing Requirements. In: COMPASS 1995: 10th Annual Conference on Computer Assurance, pp. 109–122. National Institute of Standards and Technology (1995)Google Scholar
  16. 16.
    Gargantini, A., Riccobene, E.: Automatic Model Driven Animation of SCR Specifications. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 294–309. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  17. 17.
    Morrey, I., Siddiqi, J., Hibberd, R., Buckberry, G.: A Toolset to Support the Construction and Animation of Formal Specifications. Journal of Systems and Software 41, 147–160 (1998)CrossRefGoogle Scholar
  18. 18.
    Hazel, D., Strooper, P.A., Traynor, O.: Possum: An Animator for the SUM Specification Language. In: Proceedings of 1997 Asia-Pacific Software Engineering Conference (APSEC 1997), pp. 42–51. IEEE CS Press (1997)Google Scholar
  19. 19.
    Leveson, N.G., Reese, J.D., Heimdahl, M.P.E.: SpecTRM: A CAD System for Digital Automation. In: Proceedings of 17th Digital Avionics System Conference (DASC 1998), Seattle, USA (1998)Google Scholar
  20. 20.
    Miller, T., Strooper, P.: A Framework and Tool Support for the Systematic Testing of Model-Based Specifications. ACM Transactions on Software Engineering and Methodology 12, 409–439 (2003)CrossRefGoogle Scholar
  21. 21.
    Liu, S.: Verifying Consistency and Validity of Formal Specifications by Testing. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 896–914. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  22. 22.
    Bekbay, S., Liu, S.: A Study of Japanese Software Process Practices and a Potential for Improvement Using SOFL. In: Proceedings of Third International Conference on Quality Software (QSIC 2003), Dallas, Texas, USA. IEEE Computer Society Press (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Shaoying Liu
    • 1
  1. 1.Department of Computer Science, Faculty of Computer and Information SciencesHosei UniversityJapan

Personalised recommendations