Formal methods play essential roles in education and training of software engineering. Besides the fact that formal methods themselves can be direct solutions to problems in development, many insights into modelling, speci cation, veri cation and validation can be provided. On the other hand, di culties lie in delivering these direct or indirect values to the industry. This paper reports and discusses our experience with formal methods education in the Top SE program. This program has been provided for industry engineers to learn advanced software engineering. The program contains over 10 lectures on formal methods, from theoretical foundations to practice including non-technical aspects. The program also allows the engineers to spend 3 or 6 month tackling their own problems with supervisors. Our experience in the program illustrates key factors and roles of formal methods education.
Formal methods are attracting increasing attention, as solutions to the high demand of e cient and reliable software development. On the other hand, there has been a gap between knowledge and techniques that software engineers generally have obtained and those that are required for use of formal methods. It is thus essential to provide a place where software engineers can learn formal methods and investigate their practical applications.
Formal methods can also be referred to as foundations that illustrate a set of principles and rationales in software engineering. For example, modelling vocabularies and structures in formal languages can suggest good practices in speci cation, rigorously de ning \what" (not \how"), even if encoded in natural languages. This point also suggests the signi cance of formal methods education in the general contexts of software engineering.
This paper reports and discusses our experience of formal methods education
with the Top SE program [
Among various aspects of our experience, this paper reports how the
engineers studied and evaluated formal methods to discuss key factors and roles
of formal methods education for the industry. This focus is di erent from our
previous paper in 2009 [
The remainder of the paper is organized as follows. Sections 2 and 3 give an overview of the Top SE program and formal methods education there. Section 4 provides analysis and discussion on the key factors and roles of formal methods education for the industry. Section 5 gives concluding remarks. 2
In the software engineering area, there has been a gap between what is taught
in academia and what is required by industry [
The Top SE program [
In the Top SE program, lectures are organized to involve di erent methods and tools so that students can compare di erent approaches while understanding common principles. Each class involve group exercises in which students jointly tackle practical problems while exchanging ideas on di erent approaches.
Each lecture consists of 7 or 15 slots (each slot is 1.5 hour). The 44 lectures are grouped into six \lecture series," Project Management, Requirement Engineering, Architecture, Formal Speci cation, Model Checking and Cloud Computing. Each lecture series consists of six to ten classes. As the students are industry engineers, classes are held in the evenings (6:20pm-) every weekday and in the daytime on Saturdays. Students are required to take at least six classes to graduate. About a quarter of them take this minimum number, but others take much more, in extreme cases more than 20.
3 By the Ministry of Education, Culture, Sports, Science and Technology, Japan.
Although acquisition of knowledge and exercises on methods and tools are indispensable, solving each problem requires discussions on and decisions regarding approaches such as modelling scope, right abstraction, and properties for veri cation. For exercises for such aspects, most classes have group exercises in which students jointly tackle non-trivial problems, i.e., Problem-based Learning (PBL). 2.2
The Top SE program also includes graduation studies in which students identify and tackle their own problems using approaches they have learned. The duration of the studies is 3 or 6 months, guided by a lecturer(s) as a supervisor. The studies are nally evaluated in terms of validity of problem setting, approach (methods/tools), modelling of target problems, and evaluations.
A few of typical patterns of graduation studies are illustrated below. Case Study In this type of study, engineers identify problems in development activities at their companies. They tackle these problems by selecting and tailoring scienti c methods and tools learnt in the course, and evaluate how well the problems are solved. A typical example is application of a formal veri cation tool to a typical but troublesome problem and evaluation of cost and e ectiveness.
identify problems in the application of methods and tools learnt in the course. They tackle these problems by providing ne-grained support for application, often in a domain-speci c way. A typical example is a translation tool from spreadsheets currently used for the speci c input format of a formal veri cation tool.
engineers identify problems in bridging di erent phases or tasks, for each of which methods and tools are often discussed separately. They tackle these problems by providing support for connecting output of one task to the input of another. A typical example is support of systematic mapping from requirement models to design models.
Development of Methods and Tools In this type of study, engineers identify problems in targets or capabilities of current methods and tools. They tackle these problems by constructing new methods and tools. A typical example is tool development to support deeper analysis or visualization of counterexamples generated by a model checker. 3
Our previous paper reported on formal methods education at the Top SE
program [
The class for mathematical logic teaches the set theory, predicate logic, hoarelogic, temporal logic, and so on. The knowledge is given basically from the viewpoint of \users" of the theories, e.g., those who do not prove soundness.
The other 12 classes are divided in two categories, 6 for formal speci cation
and 6 for model checking. Each category starts with a basic class that focuses on
one method, VDM [
Other examples of group exercises include robots of the classical \dining philosopher" problem. This is an extension of the classical problem since the robots can act in parallel, e.g., leading to a state in which two robots touch one folk at the same time. It is also possible to run actual robots by using the models. Discussions include how to de ne abstract and essential state transitions, what properties to verify, and so on.
Classes for Practice Two classes for practice were introduced to formal specication and model checking. The lecturers for these classes are from the industry and have application experience of formal methods.
Both classes teach principles and practice on technical or non-technical aspects, such as extraction of models from speci cation as well as communication and understanding within the team. The lecturers also deliver insightsdrwon from their experiences, such as the signi cance to explain the cost and bene t, the fact that formal methods is just one of possible means, and so on.
In the practice class for formal speci cation, students list questions regarding issues about speci cation in general and formal methods. Discussions are conducted concerning possible answers and rebuttals. The results for the rst few years led to a list of over 100 FAQs. In recent years, the list has ben discussed in a shorter time and discussions moved to a new topic: decisions and planning necessary for speci cation (when natural languages are used and when formal speci cation languages are used).
In the practice class for model checking, each student plays the role as an expert of model checking, who is asked to support a project given a speci cation document or source code. He/she is responsible for not only checking but also presenting the work plan as well as reporting of the cost and bene t.
Very Di cult Di cult Normal Easy Basic (FS) 10.2% (5/49) 38.8% (19/49) 46.9% (23/49) 4.1% (2/49) Basic (MC) 7.1% (3/42) 71.4% (30/42) 19.0% (8/42) 2.4% (1/42) Practice (FS) 13.3% (2/15) 26.7% (4/15) 53.3% (8/15) 6.7% (1/15) Practice (MC) 0% (0/9) 33.3% (3/9) 66.7% (6/9) 0% (0/9)
Table 1. Di culties There have been many studies that constantly use formal methods. For example, there were 11 studies among 41 studies for students who entered in 2013. The best award studies, 1-3 selected each year, included at least one study on formal methods. These points are discussed in detail in the following section. 4
This section extracts some data from our experience in the Top SE program and discusses key factors and roles of formal methods education in the whole software engineering. 4.1
Di culties Table 1 in concerned with di culties. Although the basic classes are the starting points, many students felt they were di cult, though not too much. Many comments for both classes included di culties due to being unfamiliar and new to logic expressions. Model checking was thought more di cult. This is probably because the problems are complex with concurrency, while the basic class for formal speci cation primarily focuses on sequential speci cation animation. The practice classes were not thought di cult since practical issues, such as management, were the main topics. A few students thought such issues were the really di cult ones, which do not have absolutely right answers and require a wide viewpoint.
Practicality Table 2 is concerned with the availability of practical information. The fundamental classes involve non-trivial group exercises and give guidelines such as modelling patterns and mapping from UML diagrams to formal models. Although some students mentioned this was very su cient, most thought it was not. The practice classes complement this point, and most students seemed satis ed with the practice classes. Most of the positive comments suggested that the students liked the \real" nature of the exercise problems, guidance for reporting, and so on. A few negative comments on the practice class for formal speci cation required more details, which were di cult to provide in the limited time of the lectures.
Applicability Table 3 shows the applicability of the obtained approaches. Even though the students liked the content of the classes, many had some doubts on the immediate applicability. This point did not change much even with the satisfaction of the practice classes.
Typical directions of positive comments are given below. { Positive comments often included speci c applications and aspects, for which each commenter felt that formal methods can be (cost-)e ective. { Some comments included \what is left should be done by each project and team," suggesting that there were some gaps but the students thought the gaps cannot be bridged in a general way. { Notable comments of non-negligible numbers were about immediate applicability of \ways of thinking," not the methods or tools themselves. For example, some included the use of principles for speci cation in natural languages, such as structuring of information and clari cation of properties. This point suggests learning formal methods allows the learning of principles signi cant in handling issues of early phases. On the other hand, these types of comments imply doubts on applicability of methods or tools themselves, as suggested from negative comments.
These positive results are encouraging, as they show that the students understood and could imagine how each project and team nally nd and tailor solutions for themselves, without any \silver bullets."
Typical negative comments were as follows. { Many comments included that the languages and methods seem too special compared with the currently available practice and skills. The students could not imagine how they are disseminated and used immediately back at their companies. { There were comments that require the methods and tools to have more useful functions. This point is true compared with popular tools such as programming IDEs. { Some comments for the basic classes suggested that the students could not imagine concrete applications. This type of comment indicates the need for the practice classes and does not appear in the comments for the practice classes.
From the viewpoint of education, it is good to see many negative comments
accompany positive comments regarding the experiences and ways of thinking
the students obtained. However, the negative comments also show long-lasting
issues on applicability of formal methods, e.g., as discussed in [
Popularity In Section 3.2, we explained the number of graduation studies as
recently being about a quarter of the number of all the studies. This number is
actually smaller compared with the previous report, in which studies on formal
methods were about half of all studies [
The current ratio of studies with formal methods (a quarter) is quite fair, which is almost the same as the ratio of formal methods classes among the total number of classes.
Quality At least one study on formal methods received best awards every year. This is probably because outputs with formal methods are clearer and more repeatable and often realized as frameworks or tools with objective rationales (compared with methods that guide human thinking on requirements, risks or architectures). This point never implies any superiority of formal methods. In any case, clari cation of required human e orts is signi cant, as well as validation of the meaning and impact of the studies.
Nevertheless, formal methods provide good opportunities for students to discuss and de ne approaches to be rigorous, repeatable, objective, and general. We discussed the latest status of our experience with formal methods education in the Top SE program. Although it is di cult to empirically prove any direct or indirect e ect of formal methods education, we have reasonable con dence in the following topics we focused on in this paper: { Key factors in formal methods education for the industry
Lecturers from the industry Delivering, working out, and discussing practice including non-technical aspects, such as planning and reporting. { Roles of formal methods in software engineering education and training Opportunities through exercises to discuss and de ne approaches to be rigorous, repeatable, objective, and general.
Clear principles, especially in early phases of development processes, which can be applied to processes without formal methods.
The Top SE program has been established to be sustainable as a paid course, accepting over 40 students from companies every year. We would like to have more experience and provide more insights into education as well as academiaindustry collaborations.
We would like to thank all the lecturers and students (engineers) involved in the Top SE program.