Engineering disciplines, as well as other science-based disciplines such as medicine, are characterised by high levels of standardisation and the subsequent availability of readily applicable handbook knowledge. In those engineering or applied science disciplines, a handbook compiling the key concepts, terms and activities that constitute a professional domain can be found in the book shelf or on the desk of every serious practitioner. From a science-philosophical point of view, the contents of such handbooks is often presented in nomopragmatic logical form [Bu98].
Formal methods in software science and software engineering have existed at least as long as the term “software engineering” (NATO Science Conference, Garmisch, 1968) itself. In many engineering-based application areas, such as in the railway domain, formal methods have reached a level of maturity that already enables the compilation of a so-called body of knowledge (abbreviated as “BOK”). Its various methods and techniques include algebraic specification, process-algebraic modelling and verification, Petri nets, fuzzy logics, etc. For example, the B-method has been used successfully to verify the most relevant parts of a model of the Metro underground railway system of the city of Paris (France). Software tool support is already available for a number of those formal methods; for example in the form of various model checker or SAT solver programs.
In this context, our workshop shall bring together scientists, researchers and practitioners, from academia, the industry, professional guildes and engineering associations, national or international standardisation committees, as well as governmental or administrative regulators to re-collect and discuss the “state of the art” in the application of formal methods within the railway domain (including inner-city tram lines, urban mono-rail systems, etc., too). Thereby we shall adopt a methodological viewpoint based on Vincenti’s book [Vi90], which contains a science-historical and science-philosophical analysis of what it is that constitutes engineering knowledge (and the related practice) specficially, in other words: an epistemology of engineering. The development of the above-mentioned handbooks as an explicit recording of such knowledge is part of Vincenti’s epistemology.
In his book [Vi90] Vincenti has thus made an attempt to understand the “nature” and practice of engineering. In the context of discussing the focus of engineers’ activities, Vincenti talked about “normal design” (obviously related to Kuhn’s “normal science” [Ku62]) as comprising “the improvement of the accepted tradition or its application under ‘new or more stringent conditions’”. He went on to say: “The engineer engaged in such design knows at the outset how the device in question works, what are its customary features, and that, if properly designed along such lines, it has good likelihood of accomplishing the desired task”.
In [Ja97], discussing his understanding of engineering practice based on a reading of Vincenti, Michael Jackson stated: “An engineering handbook is not a compendium of fundamental principles; but it does contain a corpus of rules and procedures by which it has been found that those principles can be most easily and effectively applied to the particular design tasks established in the field. The outline design is already given, determined by the established needs and products”.
An implied, though not explicitly stated view of engineering-design is that engineers normally design “devices” as opposed to “systems“. A device, in this sense, is an entity whose design principles are well defined, well structured and subject to the principles and conditions of normal design. A system on the contrary, as a subject of so-called “radical design“, is an entity, which lacks some important characteristics making normal design possible, (whereby the notion of “radical design” in engineering corresponds quite well to Kuhn’s notion of “science in crisis” [Ku62] in the domain of the pure sciences). Examples of the former, given by Vincenti, are airplanes, electric generators, turret lathes, whereas examples of the latter are airlines, electric-power systems and automobile factories. It would thus appear that systems become devices when their design attains the status of being normal. That is: the level of original creativity required in their design becomes one of systematic choice, based on well-defined analysis, in the context of standard definitions and criteria developed and agreed by engineers, in an analytical-industrial manner.
With a similar intent in mind, the Informatics theorist Dirk Siefkes had spoken about so-called “small systems” which have much in common with what Vincenti had called “devices”. In [Si92], Siefkes “called a system small, if it is in every aspect adequate, not exaggerated, and not too little”. Thus: what Vincenti’s “devices” and Siefke’s “small systems” have in common, from a philosophical point of view, is that both refer to something which is reasonably familiar, hence manageable, and thus “makes sense” to us in a pragmatic-hermeneutical manner. Both notions are thus related to the ontological notion of “Zeug” (i.e.: “equipment”) by the phenomenologist philosopher Martin Heidegger in his seminal book, Sein und Zeit (Being and Time) [He27]. The things of “Zeug” populate our medium-scale “meso” world, thus: “Zeug” is neither too large nor too small for us, since we grow up with “Zeug” in a quasi-natural manner, prior to any further philosophical reflection.
Jackson added in [Ja97]: “The methods of value (to engineers) are micro-methods, closely tailored to the tasks of developing particular well-understood parts of particular well-understood products”.
A fundamental task of software engineering research is to build a catalogue of such “micro-methods” to support the everyday work of software engineers. The aim of our workshop is thus to begin the process of devising a handbook for the application of formal methods in the railway domain. We restrict our scope to safety and control systems in this domain and, in particular, the role of software in those things.
- [Bu98] Mario BUNGE, Philosophy of Science: Volume Two, Chapter 11 (Action), Transaction Publ., 1998.
- [He27] Martin HEIDEGGER, Sein und Zeit, Niemeyer-Verlag, 1927.
- [Ja97] Michael JACKSON, Draft of a Foreword to a Collection of Papers on Formal Methods Technology Transfer, private communication, 1997.
- [Ku62] Thomas KUHN, The Structure of Scientific Revolutions, University of Chicago Press, 1962.
- [Si92] Dirk SIEFKES, Sinn im Formalen?, pp. 97-114 in Wolfgang Coy et al. (eds.), Sichtweisen der Informatik, Vieweg-Verlag, 1992.
- [Vi90] Walter VINCENTI, What Engineers know and how they know it: Analytical Studies from Aeronautical History, John Hopkins University Press, 1990.