From the Bulletin of EATCS No. 96#

A Dialogue about Formal Methods with Professor Dines Bjørner#

by Cris Calude

Professor Dines Bjørner is a well-known computing scientist working onformal methods for the specification, development and verfication of software and hardware systems. Professor Bjørner worked on VDM: the Vienna Development Method at IBM and was involved in producing RAISE: the Rigorous Approach to Industrial Software Engineering formal method and tools support.

He co-founded VDM-Europe, which subsequently became FME: Formal Methods Europe, an organisation that supports conferences, education and related activities and ForTIA: the Formal Techniques lndustry Association. Professor Bjørner’s Chef D’oeuvre is a 3-volume book Software Engineering published in 2005-2006 by Springer. He is a knight of the Order of the Dannebrog and a winner ofthe John von Neumann Medal (1994) and the Ths. Masaryk Gold Medal (1996), has received a Drh.c. from the Masaryk University (2004), is a member of the Academia Europaea (1989) and the Russian Academy of Natural Sciences (AB) (2001), and is a Fellow ofthe IEEE (2004) and ACM (2005).

Cristian Calude: Could we start by telling us the subject of your PhD Thesis?

Dines Bjørner: A ha ! Yes, I thought one associated with EATCS would ask that question. The title of the PhD thesis (1969) was: The Theory of Finite State Transductions. I have much regretted the "The". At most an "A" might have been more appropriate. In effect I had no tutor; no one at my department, for the last 2/3 of my study, had any background in computer science, let alone in automata theory and formal languages.

But a Danish PhD is not the highest academic degree one can obtain in Denmark, A PhD is society’s blue stamp of approval. Institutions hiring PhDs should be assured that PhDs from the Technical University of Denmark can be put to do advanced engineering and applied research work.

There is also, for example, a doctor technices degree. To obtain such a degree one has to have shown more than ability, One has to have also demonstrated that one’s research has influenced engineering in industry, Normally technical universities should not appoint (full) professors unless they have a Dr. techn. degree. Well, I had not at age 38, when I became a full professor, having spent 11 of my professional years, since my MSc. degree, at IBM, accumulated much in the direction of original, "path-breaking" work worthy of a dr. techn, degree. And, it was then customary that a Royally appointed professor not consider submitting a Dr. techn, thesis, Can you imagine what would happen if it was rejected ! Would that professor have to step down ?

But, I retired in early 2007. At that time I had begun writing my Dr. techn, thesis. It is based on my studies of software development methods, in particular programming methodology. The thesis was submitted in August 2008. The subject of my Dr. techn, thesis Software Engineering — an Unended Quest[1] is a careful review of my three volume Springer book on Software Engineering: Did I achieve what I set out to achieve in my research since my IBM Vienna Laboratory days (1970—1973)? Where do I think I have succeeded, where could contributions be sharpened, which methodology issues had I neglected, etc.?

CC: When did you join the EATCS?

DB: I believe it was in the late 1970s. The EATCS is the right organisation for European computer scientists. I would wish it also covered computing science. (Instead we have a bewildering set of Programming, Software Engineering, etc. associations — each founded by someone who wanted to be “President”,) To me a distinction is necessary: Computer science is the study and knowledge of the things that can exist "inside" computers as well as the science of the special techniques and theories of how computer science is pursued. Computing science is the study and knowledge of how to construct those things that can exist "inside" computers as well as the study and knowledge of how to apply the techniques of computing science to other than software (and hardware).

CC: Please reminiscence about your relation with the Bulletin.

DB: Grzegorz (Rozenberg) asked me, in the late 1970s, or was it in the very early 1980s, to orchestrate a funding drive to cover the EATCS membership for colleagues in Eastern Europe and the (then) USSR. I had travelled somewhat in several of these countries by then. The EATCS lend me their then current membership list and I wrote to "all" members asking them to contribute, Their willingness was most gratifying. And the EATCS was able to provide up towards 200 memberships — I think — and for several years.

Grzegorz — what a man, without outgoing, active, almost "shameless", people like him where would we all be? — also invited a private informatics R&D center of which I was one of the two initiators, DDC: Dansk Datamatik Center, to become an EATCS sponsor. So DDC was an EATCS sponsor for almost eight years. Later, when I “co-founded" and directed UNU-IIST: the United Nations International Institute for Software Technology, UNU-IIST became an EATCS sponsor — at least in the years I was the director on that, I shamelessly pronounce, very successful research and post-graduate/post-doctoral training centre in Macau.

CC: Do you consider yourself mainly a computer scientist, a computing scientist or a superposition of both?

DB: I consider myself a computing scientist.

CC: What is your view on "software engineering"?

DB: Software engineering is applied computing science, Most software engineer- ing textbooks, in my opinion, fail to cover advances in computing science, such as formal techniques.

CC: What do you mean by "domain", "domain engineering" and "domain modelling"?

DB: By domain is understood a universe of discourse, such as physics, literature, musicology, banking, etc. Something for which there is a reasonably delineated set of terms that cover the simple entities, functions, events and behaviours of the domain: (i) entities that represent phenomena of the domain that one can point to (i.e., seen), smelled, touched, heard, tasted, or be measured by physical (incl. chemical) instruments, or that one can conceptualise from these simple entities or concepts thereof — with some subset of observed domain entities defining a domain state concept; (ii) functions that apply to entities and yield entities, i.e., functions that observe properties of entities, parts of entities, or create new entities, etc.; (iii) events that "occur", in some domain state, and, usually, change that state (that is: events are characterised by certain predicates and transition relations over states); and (iv) behaviours — set of sequences of applied functions, i.e., actions, and events, Examples of domains are: (a) the container line industry, (b) the financial service industry, (c) railway systems; (d) "the market" (consumers, retailers, whole salers, producers and the supply chain); (e) health-care; etc.

By domain engineering is understood the analysis and description of a(ny) domain. Many stages and steps are needed to do proper domain engineering: identification of domain stake holders, domain acquisition, domain analysis, domain terminologisation, domain modelling, domain verification, domain validation and domain theory formation. Some of these stages (and/or their embedded steps) are of pragmatic nature, but several (most in terms of time spent on pursuing these stages) are based on computing science — and domain theory formation requires deep insight into computer science.

By domain modelling is understood the specific tasks of creating a domain model in the form of a precisely narrated and — hopefully also — a precisely formalised description of the domain. The descriptions are of the domain, as it is, with no reference to requirements let alone software.

CC: How relevant is theory for software engineering?

DB: "There is nothing so practical, that is, of use in engineering, as a good theory”, someone[2] is quoted to have said. The techniques of software engineering, whether for domains, requirements or software, mostly have a theoretical foundation. Where physics deals with what can be measured and hence favours such mathematics that can express measurable properties, software engineering deals primarily with domains about which we wish to express logic properties. Where classical mathematics focuses on continuity, computer & computing science, the theory-foundations of software engineering, deals with discreteness and hence modern algebra plays a role alongside mathematical logic.

A cornerstone of today software engineering, and hence a central focal point of computing science research is ‘formal specification’ and ‘verification’. A number of formal specification languages and related proof systems have evolved over the years. The first, a pan from classical predicate calculus, was VDM. Some others are, in more or less chronological order, Z, RSL (RAISE), B, Event B, Casl, CafeOBJ, ASM and Alloy.[3] Using anyone of these the software engineer can express dynamically evolving systems that grow and shrink in number of entities etc., something that classical calculus is not good at. Early notations of automata and formal language theory are steeped, it seems to me, in classi cal discrete mathematics — where use of the more modern formal specification languages, in addition to rather sophisticated theorem proving systems, is more appropriate for expressing much of today computer science work. The result is twofold: (i) published papers that attempt to formalise some, otherwise fascinating software-relevant notations or techniques, are fraught with errors, and (ii) the creators of these notations and techniques remain ignorant of progress in com puting science and software engineering. A derivative, but far more "dangerous" effect, is that many of our candidates remain sceptical of formal techniques since their teachers never took these seriously. This is a strange phenomenon: It is normal to expect that all mathematicians of a mathematics department understand basic tenets of all the branches of mathematics that are taught to students. But not so in the average computer science department. It is a disgrace.

CC: Can you comment one of your most preferred results?

DB: Well, first of all, since I work in programming methodology: the study of the sets of principles whereby the phases, stages and steps of software development can select analysis and synthesis techniques and tools. The results are not simple 18 page papers where some beautiful set of theorems are postulated and proved. The results are bits and pieces, "bricks and mortar", of methods. Together with (the late) Hans Bekič, Cliff Jones and Peter Lucas, I was one of the originators of VDM — whose VDM-SL was the first ISO standardised formal specification language. And I instigated and co-led the work that led to RAISEs RSL. So I consider my contributions here to be among my "preferred results". But, in the last 20 years my work has been focused, not on the further research into fomial specification languages and their proof systems, but in conceiving of the concept of Domain Engineering and by populating that concept with a number of principles and techniques; and in conceiving of how one can "derive", major formalisable parts of requirement prescriptions in a systematic theory-based manner — those results, I think, will stand and ought to lead to a rather dramatic reappraisal of so-called requirements engineering. I am of the unabashed opinion that core parts of today research into requirements engineering is seriously flawed. Before software can be developed one must understand its requirements. But before requirement prescriptions can be developed one must understand the domain. Electronics, automotive, aeronautics & aerospace, etc., engineers all have a sound education in physics and a specifically deep one in those areas of physics that are related directly to their engineering field: plasmaphysics, mechanics and aerodynamics & celestial mechanics. So they understand their domain. Not so for today’s software engineers. Oh, well, yes, for those who develop compilers, database management systems and operating systems. But not those, and they are the vast majority, who develop software for container lines, banks, railways, the market, hospitals, etc. Most computer science and informatics departments, by far the majority, does not offer anyway near a professional degree in software engineering. My founding and directing UNU-IIST, the UN University’s Intl. Inst. For Softw. Technology, based in Macau, China SAR, I also count as one of my "preferred results". Go see for yourself: www.iist.unu.edu.

CC: You worked for companies and universities. Can you please compare life at IBM with that at the Technical University of Denmark or JAIST?

DB: IBM, in my years, 1962-1976, was a very good company — also for us development engineers (62—70) and researchers (70—76). But a software development methodology, such as VDM, first conceived at the IBM Vienna Lab. (73-75), should not be developed in a competition and proht-oriented company, whether IBM or other. IBM’s decision not to make room for the R&D of VDM inside IBM was a ‘blessing in disguise’. VDM would never have thrived if only inside IBM. Such software development techniques should primarily be R&D’ed in open, peer-reviewed research centres — and those you found, in the past, in universities. So IBM offered great management, good salaries and exciting projects, Universities offer poor management, low salaries and freedom to pursue what is important. Well, the last seems to be a bit of a problem these days, Today informatics departments have, however, now a serious problem. Due to political pressures, spurred on by industry spokesmen, our informatics departments are caving into teaching"ready-to-wear" subjects, viz. Database design using Oracle SQL-developer version 1.5.2 or Microsoft Project Standard 2007, etc. There is nothing essentially wrong with these products — but they are just instantiated technology versions of more fundamental techniques and hence theories. Much progress in our sciences is getting lost by not being taught due to the far too many "ready-to-wear" courses. Hence we see that these fields (of progress) are less researched — and eventually disappear, I am rather pessimistic about a future of real education, as in German ‘bildung’, in our sciences.

CC: Your website includes links to other personal websites. How did you choose them?

DB: These personal website, www2.imm.dtu.dk/~db/homepages/, refer to such people as Robert Stephen Boyer, Luca Cardelli, Gerard J. Holzmann, Kouichi Kishida, Leslie Lamport and John McCarthy (alphabetically listed). I find their personal website worthwhile. Perhaps I like John McCarthy’s the best. I chose them for this: I know them, personally, their integrity and the fascinateing material displayed on their personal Web pages: they are not afraid to act politically incorrect.

CC: Please describe the Informatics Section of the Academia Europaea, its history and goals.

DB: You can read about Academia Europaea (AE) at www.acadeuro.org and about its Informatics Section (IS) at http://www.acadeuro.org/index.php?id=180. (By the way, you, Cris is the editor of that last set of Web pages.) AE/IS comprises a reasonably fair selection of some 80+ European computer scientists with a few overseas ones as well (cf. www.acadeuro.org/fileadmin/user_upload/Informatics/is-memberlist.html). AE/IS has organised, so far, two events, one in Budapest in 2006, cf. www.jaist.ac.jp/~bjorner/ae-is-budapest (by me), and one in Liverpool, 2008 (by you). Suggested by Wolfgang Resisig, we plan to organise an event, together with members of other AE sections (Linguistics, Literary Studies, Musicology. Social Sciences, Mathematics, Physics, Engineering, Earth & Cosmic Sciences and the four Life Sciences sections) on Models & Modelling. It should be possible for the AE/IS members to issue, on request (as has been done) or at their own volition, as will be done, 3-5 page State-of-the-Informatics Sciences manifestos or position papers that could advise national govemment, international organisations, the EU Commission, for example its newly founded EIT, etc., on crucial issues before these institutions. The field of computer, computing and informatics science is far from enjoying the status, neither among fellow scientists, at university management levels and in relevant national ministries, that I think it ought to enjoy. AE/IS should try to address this problem. But first AE/IS need to delineate in a reasonable fashion the field of informatics. I was the chairman of AE/IS from early 2004 till April 2009. In my time as chairman we enlarged our membership from 23 members to 83.

CC: Your latest book will appear in Japan in 2009: Domain Engineering. Could you give us details?

DB: This JAIST Research Monograph (ISBN 978-4-903092-17-l) binds, under one cover, ten (10) reports that I wrote during my one year sabbatical in 2006 at JAIST. You can all request that monograph from Prof. Kokichi Futatsugi, 1-l, Asahidai, Nomi, Ishikawa 923-1292 Japan. My answers to your questions on domains etc. give a hint of what is contained in this monograph. The chapters and appendices of this approximately 500 page monograph span from Technology Management via Science of Domain Engineering to Experimental Evidence. You may view the monograph at www.imm.dtu.dk/~db/jaistmono.pdf. It has 76 nice photos from Japan.

CC: What does give you most pleasure in life?

DB: 43 years with my wife.

CC: Many thanks.

[1]You may wish to browse that document at http://www. imm. dtu.dk/~{}db/dr.pdf.

[2] Kurt Lewin (or James Clark Mazwell or Albert Einstein).

[3] See the Springer book: "Logics of Specification Languages" (ISBN 978-3-540-74106-0).