next up previous contents
Next: Conclusions and Further Work Up: A Survey of Formal Previous: Survey Description   Contents


Survey Analysis

The surveyed data have been collected (in abstract-syntax format) in a textual database which was subject to a number of simple «data-mining» operations available from a runnable functional specification of the courses database. The following main analytical projections were identified:

The enumeration of all courses selected per each projection is given in tabular format in appendices [*], [*] and [*], respectively. The last two are ordered by number of course units selected. Column labels in tables should be read as follows:

Institution
-- Institution name (abbreviated).
Ref
-- Local identification of module in institution (if available / applicable).
Y/S
-- Year/semester of module, wherever such a time schedule is mentioned or can be safely inferred [*].
Module
-- Module name.
Contact
-- Lecturer or contact person.
Topics/Langs/Tools
-- Acronyms of module topics, (specification) languages, notations and tools. All these entries can be looked up in the glossary of appendix [*].

A brief (quantitative) analysis of these projections follows, in the form of histograms. Concerning the first projection, we have obtained the histogram of Fig. 1which summarizes the tables of appendix [*]. It can be observed that model-oriented specification (FM06) is by far the most popular topic in the survey, followed by the teaching of concurrency (FM13) and logical foundations (FM02). A third group of topics includes model checking (cf. FM10), support for executable specification (cf. FM14) and formal semantics (FM12). Comparatively less widespread is the teaching of algebraic approaches to formal specification (topics FM04 and FM05). Last in the list is multi-paradigm specification (FM07), a topic whose relevance in industrial case-studies and scientific meetings (eg. FME symposia) is not yet mirrored in the curricula.

Another question we have tried to answer is concerned with whether courses are focussed and go deep on particular subjects, or they tend to spread over many topics in a light-weight («breadth-first») manner. Without further inspection of cross-breedings among topic areas, we found out that 47 courses focus onto one topic area only, 36 courses spread over two topic areas and 21 courses spread over three areas. All other courses remaining are even less focussed.

Figure: Number of courses per main topic area
\begin{figure}\begin{center}
\begin{histogram}{110}{60}{0}{1}{2}
\map{FM07}{1}
\...
...FM02}{27}
\map{FM13}{27}
\map{FM06}{52}\end{histogram}\end{center}\end{figure}

Concerning the second projection, we have identified 24 notations (or notation variants) and/or (specification) languages, which are listed in appendix [*] ranked by the number of courses which teach or address them [*]. Altogether, we have obtained the histogram of Fig. 2. The popularity of specification languages and methods such as Z [15] and B [1] is consistent with the widespread teaching of model-oriented specification unveiled by the previous projection. The somewhat surprising rôle of functional programming languages such as Haskell [7] and SML [5] is due to their use in animation (rapid prototyping) or to the development of libraries written in such languages which support teaching.

Figure: Number of courses per language/notation
\begin{figure}\begin{center}
\begin{histogram}{50}{100}{0}{1}{4}
\map{ELotos}{1}...
...7}
\map{SML}{7}
\map{B}{15}
\map{Z}{16}\end{histogram}\end{center}\end{figure}

Concerning the third projection, and despite the fact that 65 courses don't mention any support tools in their website description, we have identified 39 tools or (formal specification) libraries, which are listed in appendix [*] ranked by the number of courses which mention them. However, the analysis of the corresponding histogram (Fig. 3) requires some care, as it is not always obvious from websites which particular tools are being imposed or recommended. Very often, tools are not even mentioned (in particular if they are open source software) and are implicit from the context [*]. Almost half of the tools offer support for model-oriented methods such as B, Z or VDM [4]. The prominent rôle of model checking tools is to be remarked, notably SPIN [6] and UPPAAL [8].

Figure: Number of courses per tools
\begin{figure}\begin{center}
\begin{histogram}{40}{170}{0}{1}{9}
\map{Actress}{1...
...{UPPAAL}{5}
\map{SPIN}{6}
\map{VDMT}{6}\end{histogram}\end{center}\end{figure}


next up previous contents
Next: Conclusions and Further Work Up: A Survey of Formal Previous: Survey Description   Contents
2004-11-04