Formal methods provide systematic and rigorous techniques for software development and we believe that they should be part of academic software engineering education. In this paper, we describe how we included a selection of formal methods in a foundational Bachelorlevel Software Engineering course. We show how we introduce the basic elements of modeling and programming language semantics, and discuss how we address the theory and practice of model checking within the scope of the two semesters of the course.
{ In the rst term, SE 1 (6 ECTS) focuses on design: the domain level and modeling languages, addressing and contrasting traditional vs. agile software development. It introduces model-driven (MDSD) approaches, domain-speci c languages (DSLs) as fundamental feature of MDSD approaches, and metamodeling as a tool for determining the abstract syntax of a DSL. While the focus is on the concepts and the modeling attitudes underlying these approaches and technologies, some of them are practiced using corresponding analysis and modeling tools. { In the second term, SE 2 (6 ECTS) focuses on development: it emphasizes the technical level, with an introduction to IT project management, and software architecture, object-oriented design, testing, maintenance and reengineering. It addresses now in practice all the phases of software development described in the SE 1, supplemented by more modern topics like Design by Contract ("When the type system of the language is not enough"), Enterprise Application Architectures and Software Product Lines (SPL). { In the concomitant project, students work together in small teams of 4-5 members to solve a more complex software engineering design (SE 1) and development (SE 2) task, applying to this case study the concepts and methods introduced in the lectures and the techniques and tools presented in the tutorials and labs. { The course assessment consists of an individual nal exam (written, 50% of the nal grade) and the evaluation of the project deliverables: the nal software product and the group reports (intermediate and nal), in total again 50% of the nal grade.
In this paper we present the course concept and report on our experiences from almost ve years of conducting the course. In particular, we discuss how we address the theory and practice of formal methods on the basis of formal semantics and model checking. The paper is structured as follows: In the following section we explain in greater detail how we placed formal method contents in the reformed Software Engineering courses. Section 3 then focusses on the model checking aspects. Section 4 discusses the learning outcomes and competencies attained by the students of this course, and Section 5 concludes the paper with a review of experiences and some lessons learned. 2
The new course aims at a foundational and experiential education, for which we
included four formal methods blocks.
1. Model Checking [
Model checking [
We introduce it in the context of model-based software development, as an early detection technique that supports validation in the speci cation and design phase, prior to implementation. We show how it is useful to analyze global model properties, where syntax or type checking at the component level is not su cient. Constraints are checked at modeling time, without execution, which o ers another range of addressable issues in addition to local validation and usual debugging methods. We also show that the list of properties against which the model is evaluated is easily extensible: including a new constraint in the veri cation only requires to provide a formula expressing the property of interest.
Consistent with our hands-on experiential approach, we introduce early in the
course the jABC process modeling framework [
Describing System Behavior The lecture introduces the basic concepts of
process modeling, Service Logic Graphs and XMDD (eXtreme Model-Driven
Development [
SLGs as Formal Models As suitable abstract model structure, we
introduce Kripke Structures, Labeled Transition Systems and Kripke Transition
Systems. Semantically, SLGs are in fact Kripke Transition Systems (cf. [
Temporal Logic Properties as Constraints Starting from the
propositional logic already familiar to the students, we introduce Hennessy Milner Logic
(HML) [
Model Checking Finally, we explain how SLGs can be viewed as Kripke Transition Systems, how to use GEAR to assign atomic propositions to the SIBs of the SLGs, how to enter logical formulas, and how to check and debug systems with GEAR. The use of GEAR is demonstrated by means of some simple examples, where the level of the student's independence is increased.
For these examples we use processes that are modeled as SLGs using only Prototype SIBs, like the abstract web shop process shown in Figure 1 (top). These SIBs are pure modeling means, as they do not have an actual implementation, but as the implementation is not relevant with regard to this kind of abstract model checking, they are su cient for the purpose. Then system requirements are formulated as temporal properties. The lab discusses interactively which atomic properties (APs) need to be assigned to which nodes (SIB instances) and how to capture the formulated requirements as CTL formulas. The students use the AP inspector to annotate SIB instances with the atomic propositions, with results similar to the display in Figure 1 (bottom).
With the GEAR formula manager, students can edit CTL formulas and document them with natural-language descriptions (see Figure 2, left). The model checking inspector displays all currently available properties, and one can toggle between the formulas and their high-level descriptions. In the hands-on sessions, students learn to check all properties, nding out which hold for the entire model (i.e. for the start SIB) as in Figure 2 (right), or individually for each node in the model. This check mode can also be applied to individual formulas: the nodes where the formula holds/does not hold are highlighted by green/red boxes respectively, as shown in Figure 3. Please note that the small examples in the
gures are meant for illustration purposes only, and that the examples on which the students work in their projects are larger and more complex.
After the lessons, tutorials, and introductory labs, the students are required to design a more complex jABC process, express relevant process properties, and check them with GEAR, in a project that mimics a system design from scratch. The concrete project task in SE 1 concerns rst the user requirements for a sample Software Engineering project. Solutions are built in three steps: 1. Building a system speci cation via a UML Use Case Diagram supplemented by documented and prioritized use cases. The scenarios (system behaviors) corresponding to the use cases must be speci ed as process models, some as UML Activity Diagrams and some as SLGs. This way the students compare two exemplary modeling languages, learning to evaluate similar technologies wrt. adequacy for a speci c purpose. 2. Developing a prototype of the system, delivering an executable SLG validated through the Tracer. For this process model, the students need to specify several global behavioral properties and verify them using the GEAR. 3. Documenting and evaluating the project activities and management decisions of the group, as a third part of their project solution and report.
In SE 2, the students continue the project towards the implemented product: structural design (architecture and class model) and a documented implementation, tested by unit tests. As it often happens in real software projects, in the second term they do not continue with their own speci cations, but they must take over the speci cation from a di erent SE 1 team, whenever possible based on a di erent user story (i.e. a di erent system). They start over with the assessment of plausibility, feasibility, completeness, and quality of the previous group's deliverable and then they complete the speci cations to a point where they feel comfortable with moving to the design and implementation. 4
We describe the formal methods-related skills that the students acquire in our Software Engineering course in terms of the following competence elds: { Professional competencies: Graduates of this course have broad knowledge about languages for the modeling of software. They know the principles and theoretical foundations of model checking. { Methodological competencies: They are able to use selected languages and tools for the process- and object-oriented modeling of software. They can apply model checking for the formal veri cation of process models. They can assess/check the meaning of programs and their corresponding ow graphs using structural operational semantics (SOS). They are familiar with the use of logic calculi (axiomatic deduction systems). { Action competencies: They are able to include formal veri cation methods in their software projects in addition to traditional validation and testing.
The course has so far been attended by over 250 students. Approximately half of the participants were enrolled in the B.Sc. Computer Science (2010-2014) or B.Sc. Computational Science (2015); the other half were students in the B.Sc. Business Informatics. There has been no observable di erence between these groups regarding the achievements in the exercises, exams and projects. We saw however a signi cant di erence among the skills developed by these students and those of the precedent years: While the previous generations were more con dent in architectural issues and coding skills, our students have a more intuitive con dence with application development and with mastering a number of different technologies. We saw the advantage of this abstract and behavior-driven modeling in their approach to the subsequent module on Foundations of Service Engineering, where the black-box character of components is really central. The familiarity with the basic formal methods concepts was also advantageous in the subsequent specialistic course on Formal Methods in System Design (FMSD): taught in an e-learning fashion via teleconference-based lectures shared with the TU Dortmund and complemented by local tutorials and labs, it was clear that the Potsdam students had a smoother approach to the more technical material in FMSD due to their previous experience with the basic concepts. 5
We strongly believe that today, facing service orientation and an increasing interest in user-de ned business processes, lightweight formal methods should be integral part of the standard academic software engineering education. Accordingly, since 2010 we have been teaching a foundational Bachelor-level Software Engineering course with four embedded formal methods components at the University of Potsdam.
We chose on purpose only so-called "lightweight" formal methods, i.e. such that algorithms exist (like type checkers and model checkers), and not theorem provers or proof techniques for program correctness like Hoare style program veri cation (both presented at length in other courses), because we wished to provide scalable approaches that have a low threshold to adoption, ease of reasonably con dent use in the small, and a high ease of embedding in a full edged model driven IDE (for us the jABC). While high-end Formal Methods continue to require a deep knowledge of the mathematical concepts and formalisms, we believe that IDE-embedded FMs should be made available systematically to the next generation of Software Engineers as part of their basic profession-oriented education. Like basic English has successfully become within a generation a standard in the schools, establishing itself culturally as the "lingua franca" of international communication, the ability to take a domain-speci c perspective, to think in terms of domain speci c properties, to formulate them in such a way that both a user and a tool are able to work with them, and the ability to conduct veri cations on early models of a system are in our opinion the key to a better understanding between IT professionals, in particular Software Engineers.
Another advantage is the ingrained sense of accountability and ownership that comes with the ability and habit of verifying early and verifying often, by means of tools that take an objective perspective (other than user inspections) and provide a third party repeatable outcome. With all the limitations and drawbacks that we know of the FM tools and approaches we have today, such a step towards accountability for decisions and outcomes early in the design constitutes in our opinion a central shift towards maturity of the professional gure, competence beyond the production of code, and ultimately towards establishing a new concept of ethics and responsibility in the Software Engineering profession.