Abstract
In order to make practical use of formal methods, it is not sufficient for engineers to obtain general, fundamental knowledge of the methods and tools. Actually, it is also necessary for them to carefully consider their own contexts and determine adequate approaches to their own problems. Specifically, engineers need to choose adequate methods and tools, determine their usage strategies, and even customize or extend them for their effective and efficient use. Regarding the point, this paper reports and discusses experiences on education of formal methods in the Top SE program targeting software engineers in the industry. The program involves education of a variety of scientific methods and tools with group exercises on practical problems, allowing students to compare different approaches while understanding common principles. In addition, the program involves graduation studies where each student identifies and tackles their own problems. Statistics on problem settings in the graduation studies provide interesting insights into what top-level engineers tackles after learning formal methods.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Honiden, S., Tahara, Y., Yoshioka, N., Taguchi, K., Washizaki, H.: Top SE: Educating Superarchitects Who Can Apply Software Engineering Tools to Practical Development in Japan. In: The 29th International Conference on Software Engineering, pp. 708–718 (2007)
Top SE project (NII), http://www.topse.jp/
Beckman, K., Coulter, N., Khajenoori, S., Mead, N.R.: Collaborations: Closing the industry-academia gap. IEEE Software 14(6), 49–57 (1997)
SPIN - formal verification, http://spinroot.com/
LTSA - Labelled Transition System Analyser, http://www.doc.ic.ac.uk/ltsa/
The SMV System, http://www.cs.cmu.edu/~modelcheck/smv.html
UPPAAL, http://www.uppaal.com/
Formal Systems (Europe) Ltd., http://www.fsel.com/
Communicating Sequential Processes for Java (JCSP), http://www.cs.kent.ac.uk/projects/ofa/jcsp/
B Method - Presentation of B Method, B Language, and formal methods, http://www.bmethod.com/
VDM information web site, http://www.vdmtools.jp/
Rodin - rigorous open development environment for complex systems, http://rodin.cs.ncl.ac.uk/
Saaltink, M.: The Z/EVES System. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)
The Java Modeling Language (JML), http://www.cs.ucf.edu/~leavens/JML/
Java PathFinder, http://javapathfinder.sourceforge.net/ (last Access, April 2008)
Artho, C., Taguchi, K., Tahara, Y., Honiden, S., Tanabe, Y.: Teaching software model checking. In: Formal Methods in Computer Science Education, FORMED 2008 (2008)
BPMN information home, http://www.bpmn.org/
Kubo, A., Washizaki, H., Fukazawa, Y.: Automatic extraction and verification of page transitions in a web application. In: The 14th Asia-Pacific Software Engineering Conference, ASPEC 2007 (2007)
Goal-Driven Requirements Engineering: The KAOS Approach, http://www.info.ucl.ac.be/~avl/ReqEng.html
Nakagawa, H., Taguchi, K., Honiden, S.: Formal specification generator for KAOS: Model transformation approach to generate formal specifications from KAOS requirements models. In: The 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), pp. 531–532 (2007)
Ogawa, H., Kumeno, F., Honiden, S.: Model checking process with goal oriented requirements analysis. In: The 15th Asia-Pacific Software Engineering Conference (ASPEC 2008), pp. 377–384 (2008)
Kurita, T., Chiba, M., Nakatsugawa, Y.: Application of a Formal Specification Language in the Development of the “Mobile FeliCa” IC Chip Firmware for Embedding in Mobile Phone. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 425–429. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ishikawa, F., Taguchi, K., Yoshioka, N., Honiden, S. (2009). What Top-Level Software Engineers Tackle after Learning Formal Methods: Experiences from the Top SE Project. In: Gibbons, J., Oliveira, J.N. (eds) Teaching Formal Methods. TFM 2009. Lecture Notes in Computer Science, vol 5846. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04912-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-04912-5_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04911-8
Online ISBN: 978-3-642-04912-5
eBook Packages: Computer ScienceComputer Science (R0)