University of Iceland
Hjardarhaga 2-6
IS-107 Reykjavik, Iceland
When formal methods are taught in the Computer Science curriculum, they are often taught in a separate course and not integrated well with other methods that are semi-formal such as UML (Unified Modeling Language). At least this has been the structure of our curriculum at the University of Iceland. We have taught a short introduction to Z in a course we call Software Development in the B.S. program. In the M.S. programme we have a course called Formal methods in Software Engineering. In this course the strongest emphasis on teaching students Z but there is also an introduction to other formal methods and methodologies.
We have had success in teaching object-oriented analysis and design for a number of years. First using the OMT (Object Modeling Technique) and then UML. With increasing emphasis on safety and security and the correctness of software, we also see the need to teach formal methods for software development. This has been more apparent with standards on safety [6]. Furthermore, we have seen the advantage for students to take a semi-formal approach from the beginning when learning programming. In a first year course on programming we have taught specification of pre- and postconditions in an informal way. In that course we have taught data and loop invariants along with informal proofs.
In [1] Benediktsson reflects on how the work in progress on Software Engineering Body of Knowledge [2] applies to university curriculum development. In particular he categorises the courses according to a set of pedagogical categories called Bloom level [3]. Wing [4] has analysed how formal methods can be woven into the undergraduate computer science curriculum. She does not only look at software development as is done in this paper but the entire computer science curriculum including courses such as operating systems.
In this section we analyse what is offered at University of
Iceland (UoI) offer in terms of formal methods and the weaknesses
of the current approach. Below we state the facts about the current
curriculum with respect to formal methods. In order to classify
the level of knowledge the students have we used the Bloom classification
[2]. The categories are listed and explained
in Table 1. Further explanation can be found
in [2].
| Knowledge | Observation and recall of information |
| Comprehension | Understanding information |
| Application | Use methods, concepts, theories in new situations |
| Analysis | Seeing patterns, organisation of parts |
| Synthesis | Use old ideas to create new ones, generalise from given facts. |
Formal methods in the 1999-2000 curriculum at UoI:
The main weakness of the current undergraduate curriculum is that:
The main weakness of the graduate curriculum with respect to
formal methods is that there needs to be a better connection between
the course on formal methods with other connected courses such
as software quality management. When assessing software processes
and product quality models of a company, students need to be able
to select between heuristic and formal methods that are appropriate
to use. At the graduate level this is more linked to the software
process improvement and software product improvement at a company
level rather than at a project.
The improvements that are suggested in this section aim to remove the weaknesses stated in the previous section. We first cover the undergraduate level. The Bloom categories are italicised.
Computer Science 1 - Knowledge of informal specification.
Computer Science 2 - Application of informal pre- and postconditions. Comprehension of invariants in programming.
Logic and software development - Application of formal proofs in programming.
Software Design - Comprehension of formal methods in software development. Integration with heuristic methods
Software Project 1 and 2 Application of semi-formal and formal methods in specification, design and implementation. The student will learn how to select between heuristic and formal methods based on the requirements of the software product. This selection is based among other things on safety requirements.
The improvements for the graduate level concerns two courses:
Formal Methods in Software Development. Students should have a comprehension of several formal methods and be able to apply at least one. They should be able to make a selection of the application of a formal method in software development processes of a company. The goal is to reach the analysis level according to the Bloom classification.
Quality management system. Link the various quality standards and safety standards to the need for formal methods.
Several actions need to be taken in order to implement the improvements stated in the previous section. The course Logic and Software Development is a new course and that has to be designed to meet its objective. We do not describe the implementation further except to discuss two topics that we think we need to research further in order to implement the improvements. These topics are listed in the following two subsections. Other topics that can be discussed are how textbooks and tools meet our demand for improvements.
5.2 Integrating Z with programming languages
In code inspection, one of the things we inspect against is specification of a function. This specification may be written as text along with the function, e.g. as loosely stated pre- and postconditions. If we specify a function formally, it would be of benefit to see the code in the formal specification language like Z right along with the program code for the function. At least it should be easy for the inspector to navigate a hyperlink to the formal specification.
5.3 Integrating UML with Z
In order to implement the improvements that were suggested in the last section we need to show how we can integrate formal and heuristic methods in the course Software Design. We have taught object-oriented methods for some eight years, first using OMT and then UML when it was published. We have also taught Z but mostly at the graduate level and only once in a special topic course at the undergraduate level.
Quite a few methods have been suggested as an extension to Z that include object-oriented specification. It would be too ambitious to try to set forth in this paper an exact integration of UML with Z. However, we will pose some questions that need to be answered and attempt to outline the approach to be taken. We look at the deliverables of UML and Z and investigate how these are appropriate for different software development processes. The deliverables or diagrams that we use in UML are:
These diagrams are used through out the software development process but with different emphasis. For example, we use the use cases diagrams for requirements capture but can still refine them further in a specification phase. Later they can be used for validation of design and in acceptance testing. The same can be said for other categories of diagrams such as class diagrams. At the analysis phase, we may simply state what classes exist and their relationship. During early design we may add attributes and methods. During detailed design we will specify the signatures of the methods more clearly. Also during detailed design we may refine some relationships between classes to decide what type of tools will implement them.
If we look at the forms of deliverables of Z we have schemas and axioms. Refinement is a prominent characteristic and is used to take the developer from requirements through implementation. The question that we need to answer is how can these two methods be integrated, or put in another way: when can we benefit from using a more formal method? My hypothesis is that formal specification belongs in late requirements phase and in design, i.e. when we start to specify classes, and behaviour, i.e. how an event or a transition affects the state of a class. This is not captured very well in UML. It only captures that one object invokes another using a method. The disadvantage is that this would lead to doing the same thing twice. We would still specify classes, and their attributes and relationships in class diagrams and would have to produce Z schemas for the classes also. A solution for this may be a skeleton Z generator from UML, just as we have a skeleton C++ generator to produce C++ class descriptions from UML.
Further down the development phases, Z specifications can be
refined further to detailed design. Two other uses of the Z specifications
are useful. The first one is during code inspection. During code
inspection we verify that the code is according to specification
and I think it is important that that specification is in a formal
language. The second use is when we validate the software product
against the requirements. Table 2 illustrates
one view of the relationships that have been described in the
text. It is put forward here as a draft proposal and has not been
validated and is meant to encourage discussion.
| Phase | UML | Z | Comments |
| Requirements | Use cases | Functional specifications can be used | |
| Analysis |
Use cases refined. State and activity diagrams. Analysis classes identified and perhaps associations. Collaboration diagrams describe the use cases further by describing methods but not operators. |
Few schemas for entities and basic axioms describing relationships between entities. Schemas that describe states and transitions between states |
|
| Design |
Design class diagrams with attributes, relationships and operations Interaction diagrams |
Schemas describing classes, attributes and operations | |
| Design - detailed | Schemas for operations design. Design of relationships refined | ||
| Implementation / coding | Refinement of schemas for implementation | ||
| Implementation / code reviews | Review code with respect to Z schemas from detailed design | ||
| Test | Test cases can be done from use cases. | Test cases can be done from Z design specifications. | |
| Assessment | Review with respect to use cases and Z functional specification |
In order to put this proposed scheme to test we need to develop
a case study that would also serve as an example for the coursework.
In the integration our goal is to use the advantages of both methods.
UML provides us with diagrams that often give a good overview
of the various entities and their relationships. It also models
in a visual way the interaction, the sequence and concurrency
of the actions in the system. On the negative side it does not
model how attributes or relationships are updated as a consequence
of some action or operation. State diagrams can however model
different states and transitions between states.
The evaluation can be short term and long term. The short-term evaluation can be done after offering the new curriculum for one or two academic years. We need to assess how well we have been able to teach and what difficulties the students may have encountered. We would revise the above plan according to our findings.
The second objective of the evaluation is to see how the curriculum
has benefited graduates in their work in industry. We realise
that this may be a difficult goal to fulfil but this must however
be one of our ultimate goals, i.e. to train students for industry.
In this paper we have analysed the current curriculum at the
University of Iceland and analysed it for weaknesses in the software
engineering part with respect to formal methods. We have suggested
improvements to the curriculum and further suggested specific
actions on how to integrate formal and heuristic methods. This
work is based on our experience of teaching UML and Z separately
and not being fully satisfied with that approach. We have attempted
to develop software both using UML and Z, where one group started
with UML and then went on to Z and another group did the opposite,
that is started out with Z and then went on to UML. The result,
although the experiment was informal, gave us the motivation to
integrate the two into one track where you embed UML with Z. Another
motivation is that we have found that books on Z or formal methods
do not adequately link formal methods with the software development
processes. UML is on the same level as Z, that is it is a language
but several books have been written on how to apply UML in the
software development processes. This, indeed, is a very urgent
area for formal methods. We have only described the first step
in the improvement since we need to see how it realises in the
courses and then how it is applied in industry.