Skip to main content

Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa’s Case (Extended Abstract)

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10009))

Included in the following conference series:

  • 805 Accesses

Abstract

We have been making much effort to promote formal methods in Japan, especially Japanese IT companies. This paper describes our activities in Japan for almost twenty years, and shows typical reactions from such Japanese companies for application of formal methods. We mention about the obstacles they think to adopting formal methods in their real software development projects. On the other hand we also present a case of FeliCa Networks, Inc. as a best practice of applying formal methods in Japan. We discuss the lessons learned from our efforts of promoting formal methods and the FeliCa’s case. Finally, we briefly introduce our research project to support software developers in adopting formal approaches to real projects.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Araki, K.: Are formal methods relevant?: how to explode the seven myths in Japan. In: Proceedings of the APSEC 1995, pp. 514–515 (1995)

    Google Scholar 

  2. Araki, K., Chang, H.-M.: Formal methods in Japan: current state, problems and challenges. In: Proceedings of the Third VDM Workshop, VDM 2002 (2002)

    Google Scholar 

  3. Bowen, J.P., Hinchey, M.G.: Ten commandments of formal methods. IEEE Comput. 28(4), 56–63 (1995)

    Article  Google Scholar 

  4. Gmehlich, R., Jones, C.: Experience of deployment in the automotive industry. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 13–26. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. Hall, A.: Seven myths of formal methods. IEEE Softw. 7(5), 11–19 (1990)

    Article  Google Scholar 

  6. IPA/SEC: Report on Successful Cases of Formal Approaches with Rigorous Specification, WG on Rigorous Specification, IPA/SEC, Tokyo (2013) (in Japanese). http://sec.ipa.go.jp/reports/20130125.html

  7. Kurita, T., Nakatsugawa, Y.: The application of VDM to the industrial development of firmware for a smart card IC chip. Int. J. Softw. Inf. 3(2–3), 343–355 (2009)

    Google Scholar 

  8. Kurita, T., Ishikawa, F., Araki, K.: Practices for formal models as documents: evolution of VDM application to “Mobile FeliCa” IC chip firmware. In: Bjørner, N., Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 593–596. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  9. Kusakabe, S., Lin, H.-H., Omori, Y., Araki, K.: Developing core software requirements of energy management system forsmart campus with advanced software engineering. Int. J. New Comput. Archit. Appl. 4(1), 48–55 (2014)

    Google Scholar 

  10. Kusakabe, S., Lin, H.-H., Omori, Y., Araki, K.: Visualizing centrality of process area networks in CMMI-DEV. In: Proceedings of International Conference on Software and Systems Process (ICSSP 2015), pp. 173–174 (2015)

    Google Scholar 

  11. Oda, T., Araki, K., Larsen, P.G.: VDMPad: a lightweight IDE for exploratory VDM-SL specification. In: Proceedings of the 2015 IEEE/ACM 3rd FME Workshop on Formal Methods in Software Engineering, pp. 33–39 (2015)

    Google Scholar 

  12. Oda, T., Araki, K., Larsen, P.G.: ViennaTalk and assertch: building lightweight formal methods environments on pharo 4. In: Proceedings of the International Workshop on Smalltalk Technologies (2016, to appear)

    Google Scholar 

  13. Omori, Y., Araki, K., Larsen, P.G.: JODTool on the Overture Tool to manage formal requirement dictionaries. In: Proceedings of the 13th Overture Workshop, Co-located with FM 2015, pp. 3–17 (2015)

    Google Scholar 

  14. VDMPad Server: http://vdmpad.csce.kyushu-u.ac.jp/

  15. ViennaTalk: https://github.com/tomooda/ViennaTalk-doc

Download references

Acknowledgments

This work is partly supported by Grant-in-Aid for Scientific Research (S) 2422001.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Keijiro Araki .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Araki, K., Kurita, T. (2016). Promotion of Formal Approaches in Japanese Software Industry and a Best Practice of FeliCa’s Case (Extended Abstract). In: Ogata, K., Lawford, M., Liu, S. (eds) Formal Methods and Software Engineering. ICFEM 2016. Lecture Notes in Computer Science(), vol 10009. Springer, Cham. https://doi.org/10.1007/978-3-319-47846-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47846-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47845-6

  • Online ISBN: 978-3-319-47846-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics