Next: 3 Workshop Goals
Up: Monotonicity and Lattices as
Previous: 1 General Introduction
My scientific background is both in component-based software engineering and formal methods. Already in my diploma thesis at the Swiss Institute of Technology in Zurich, I worked on the formal development of a distributed deadlock detection algorithm [SH89]. In my M.Sc. thesis [Heu91] at the University of Victoria (Canada), I have derived an algorithm in computational geometry. The derivation has been strongly influenced by the work of Dijkstra [Dij76,DS89]. The thesis presents the development from a formal specification to an executable program.
Initially, I wrote the executable program in C++, but rewrote it as soon as the programming environment Oberon was released on an available computer. Oberon is a modular and therefore a component-based language, which has anticipated many of today's developments in object-oriented programming already in the 80's: type extension, type safety, dynamic loading, garbage collection, just to name the most important ones.
My enthusiasm for Oberon brought me back to the institute for computer systems, where Oberon had been developed by Niklaus Wirth and Jürg Gutknecht [Wir88,NW89,WG92] with their assistants. In my four years appointment, I had contact with colleague assistants, for example with Clemens Szyperski, Sepp Templ, Wolfgang Weck and Régis Crelier, who performed early experimental work in the now emerging field of component-based software systems.
Even though involved with practical programming exercises in student's assignments and projects, our international group headed by Beverly Sanders and consisting of Spiros Lalis, Martin Gitsels and myself was supposed to be mainly concerned with formal methods and its application to distributed systems. Spiros Lalis extended Oberon to a prototype distributed system [Lal94] and Martin Gitsels, whom I shared the office with, worked on a proof editor and a network protocol. My own work on various areas in distributed systems and object-oriented programming was mostly of theoretical nature using first UNITY [CM88] and later the refinement calculus [Mor94]. After that Sanders quit the institute, I joined the programming methodology group of Ralph Back in Finland. Ralph Back has been a pioneer in refinement calculus, which has a strong foundation in higher order logic and weakest precondition semantics.
Currently, I am in charge of the project ``Building Correct and Reusable Software Components in Oberon using the Refinement Calculus'' [Heu95a]. The main publications of the project are [Heu95b,Heu97e]. As a case study and practical by-product, I continue the development of the refinement tool RefStep [HH95,Heu97c]. To gain contact to other communities and experience in related methodologies, I have carried out a project [Heu96a] with the method B [Abr96] and I have published the result in [Heu96b]. Subsequently, I have been appointed to be a member of the program and steering committee of the second B conference.
Since two years, I am enrolled as a Ph.D. student at the Turku Centre of Computer Science (TUCS) and Åbo Akademi in Finland. TUCS is a graduate school that has received much attention for encouraging interdisciplinary work in computer science, mathematics and business administration. By my experience, a promising exchange of ideas exist between the disciplines of programming methodology and discrete mathematics. I argue in this position paper that a common interest focuses on the foundation of component-based systems.
Philipp Heuberger