Model Based System Development/Move or Clean UP/Methodology

Sysopsis of the project's results

Methodology

Staff

• Hanno Wupper (project leader)
• Hans Meijer
• Angelika Mader

Start: 1994 funding: none

Description

Computer science, being a comparatively young discipline, is pervaded by a Babylonian confusion of terms and concepts, with the following consequences. Technical terms-even fundamental ones like 'state', 'specification', or even 'program'-have slightly different meanings in different research areas, which does not favour communication among scientists.

Computer scientists, particularly young ones-students-may have difficulties putting results of others in context. It may be unnecessarily difficult to relate the results of computer science to those in other disciplines. Information technologists who have been trained a particular language or method may despair when they are forced to switch to another language or method and cannot see how they still can use their knowledge in the new environment. Finally it may be very hard to explain to the general public or the authorities what computer science is all about and which benefits may be expected from research programmes.

This project shall contribute to the understanding of rational system design and verification. Information technologists and teachers and students of computer science should find the way of thinking developed here helpful to disentangle complex achievements of computer science and to re-use their constituents in other contexts, but also to see what their activities have in common with other disciplines. The first papers try to answer the question what information technology is all about and what computer science has to do with it. The method is to begin with a basic, abstract and general observation ("We want machines that really do what they should do."), which is subsequently refined and detailed. This leads to definitions of a consistent set of notions with respect to which important aspects of a rational design process can be understood, together with a consistent terminology. Systematically applying Ockham's razor, we touch upon a number of divide-and-conquer-like classifications, which allows to "zoom in" more and more on specific questions.

A Taxonomy for Computing Science

The first, and most fundamental, classifications are presented in CSI-Report 9713: A Taxonomy for Computing Science (of which there is a hypertext version). All subsequent work in this project is building forth on this Taxonomy.

In our view, a rational design process is understood as an approximation of a design and verification process supported by formal methods. Of course, most information technology systems are and will be built without use of formal methods-often even without written specifications. To claim that daily practice of information technology ought to be otherwise would be unrealistic: formal correctness proofs are difficult and expensive. Nevertheless, each designer who is convinced that his machine or program does what it is supposed to do has a certain intuition that something could be proved if necessary. This project shall make that intuition more conscious and more explicit-which may lead to a better understanding of the design process and the decisions taken in its course.

Results 1998

Design as the Discovery of a Mathematical Theorem

The paper Design as the Discovery of a Mathematical Theorem - What Designers Should Know about the Art of Mathematics was presented at the Third Biennial World Conference on Integrated Design and Process Technology (IDPT) organised in Berlin by the interdisciplinary Society for Design and Process Science (SPDS). It was decorated with the Rudolf Christian Karl Diesel Best Paper Award because of its clarity and interdisciplinary view.

In 1998, Angelika Mader joined the project. She and Hanno Wupper are also doing research on formal methods for PLC programs in the framework of the hybrid systems/ VHS project. The results from the Methodology project (notions, terminology, way of thinking) have been successfully applied to the research in the VHS project: they helped in disentangling and understanding a complex area. This has, however, not led to publications in 1998.

In August 1998 a new introductory course for beginning students of informatics has been given the first time by Hanno Wupper and Erik Barendsen. This course was strongly based on the results of this project. The evaluation of the course by the participants was positive.

Results 1999

Introductory course

CSI-Report 9914: Anatomy of Computer Systems - Experiences with a new introductory informatics course. Our experiences with this course were presented at NIOC'99 under the title "Computersystemen ontleed en begrepen - Ervaringen met een nieuwe introductiecursus informatica". (The corresponding article is unfindable on the NIOC cd-rom because the editors put it in the wrong place.) The course itself got a fixed place at the beginning if the Nijmegen Informatics curriculum.

System Design as a Creative Mathematical Activity

CSI-Report 9919: System Design as a Creative Mathematical Activity - written for information technologists rather than computer scientists - explains that, although for good reasons most systems are designed without use of formal methods, it may be a source of useful insight to understand all design as an ‘approximation’ of such a mathematical activity. This leads amongst others to a taxonomy of design decisions, and it may help to relate paradigms, theories, methods, languages, and tools from different areas of computer science to each other to make optimal use of them.

A workshop on the Taxonomy was given at the NIOC'99. A hypertext-version of the Taxonomy-article was prepared and accepted for the NIOCC cd-rom. (The editors, however, forgot to include it altogether.)

Beweren en bewijzen

The course Beweren en Bewijzen, an introduction to Logic in Informatics, was completely redesigned and is now strongly based on the results of this project.

Results 2000

Wat is informatica eigenlijk?

The lecturers of the NIOC'99 workshop on the Taxonomy were invited to prepare a popular version in Dutch for TINFON. This appeared in two parts in the course of 2000. The unabbreviated version is available as CSI-Report 0008: Wat is informatica eigenlijk?

In 2000, the School of Informatics initiated a redesign of all p.r. and information material about the study of informatics in Nijmegen: folders, lectures, demonstrations, workshops for potential students became more and more based on the results of this project.

Assessment of the role of formal methods

The Taxonomy was 'instantiated' for a specific platform: PLCs. The result is a framework that allows to explain clearly where formal methods can be applied during development and verification of PLC applications and what they can and can not contribute to correctness.

Results 2001

Control specification derived from plant and requirements

The method described in Design as the Discovery of a Mathematical Theorem was applied in a case study leading to a publication in the European Journal of Control: Angelika Mader, Ed Brinksma, Hanno Wupper, Nanette Bauer: Design of a PLC Control Program for a Batch Plant, VHS Case Study 1, European Journal of Control, 2001 vol. 7, issue 4, p.416-439. abstract. Also available as technical Report CSI-R0113, March 2001.

This paper gives a complete, formal correctness theorem for a small chemical plant, where the specification of the control program has been derived as the solution of the formula:

specification of plant /\ X => requirements

The main effort was the derivation of the specification of the plant. This gave rise to new research questions, which eventually should lead to the MOCA-project in Twente.

Results 2002

Adriaan de Groot and Hanno Wupper presented A Taxonomy of Reactive Systems. technical report NIII-R0210 February 2002. It gives a consistent set of formal definitions for fundamental concepts for specification and verification of reactive systems.

Hans Meijer et al. compiled a series of books for computer science education at secondary schools: Turing, Thieme-Meulenhoff 2002. It is based on a conventional classification of the discipline, as the publishers considered it too early to base it on our taxonomy. This taxonomy, however, is presented as "an alternative perspective" in the final chapters.

Results 2003

Introductory course extended

The introductory course was doubled in size and now fills the first two weeks of the bachelor courses for both computer science and information science. The second week is hung op on the taxonomy diagram and the corresponding professional activities. More and more courses of the curriculum refer to the taxonomy.

Results 2005

Erik Barendsen en Hanno Wupper: Een academische introductie tot de informatica. TINFON - tijdschrift voor informatica-onderwijs, 14e jaargang nr. 1 (2005).

De hele opleiding in twee weken? Onderwijsvernieuwing in meerdere dimensies Onderwijsseminars FNWI Afdeling Onderwijszaken, 1 december 2005

Hans Meijer retired.

Planning 2006

Work on an extended version of the Taxonomy (viz., notions, terminology, way of thinking) toghether with the Information Science group of the NIII and the MOCA project group in Twente. Focus:what is a good correctness theorem and how to find it?