|
TSE Maibaum
|
|
|
|
|
TSE Maibaum
|
|
|
My research interests have focused for over 30 years on the theory of specification and its application in various contexts. My initial ventures in this area were with colleagues at the Pontifícia Universidade Católica do Rio de Janeiro (PUC), where I have been an Honourary Professor since 1992. The most prominent amongst these were Paulo Veloso, Roberto Lins de Carvalho and Carlos José Pereira de Lucena. We developed a first order logic approach to specification, in contrast to initial algebra approach then current in the community (which we thought was methodologically ill founded). This theory was developed over the years to deal with a range of specification issues, including parameterisation, refinement, and, eventually, modularity. The last of these focused our attention on meta theoretic aspects of specification: Why is a specification formalism good or bad for specifying particular kinds of applications? What exactly is modularity? Are there properties of formalisms that can be used to characterise their suitability?
A specific answer to the last question initiated a line of research, suggested originally by Martin Sadler (now of HP Labs Bristol), on interpolation properties of formalisms and their connection with so-called modularity properties. There is an intimate relationship between modularity and interpolation and this area of work is continuing to produce interesting results (see the recent work of Veloso and Dimitrakos).
In the early 80s, I started work on what has become known as Requirements Specification. As part of the Alvey Programme, we developed, in conjunction with several partners, a method and language to support the requirements specification of reactive/real-time systems. The project became known as the FOREST Project and the underlying formalism was called Modal Action Logic (MAL). It was a modal logic of actions, with additional operators inspired by deontic logic. Our interest in these operators was to specify causality and sequencing. Samit Khosla wrote a seminal dissertation on this topic. Many ideas now current in requirements work were prototyped on this project by Colin Potts and Anthony Finkelstein.
An interesting problem occupying us in the later stages of the project was the problem of structuring specifications. Veloso and I had already noticed that, by taking theories as units of structure in specification, we could use categorical operations, like pushouts and colimits, to build larger specifications from components. This idea had been independently noticed by a (then) young researcher visiting me at Imperial College, José Fiadeiro. He and I spent over 10 years working out the consequences of this observation in the context of MAL and temporal logics generally. We applied the ideas to develop formalisms to specify reactive systems, object oriented systems and for defining the semantics of certain object oriented structuring principles and languages (with Juan Bicarregui and Kevin Lano). We also addressed a niggling discomfort, the ontologically different worlds of programs and specifications and the obfuscation in specification theories of these differences. We developed a "toy" language called COMMUNITY, in terms of which the difference could be characterised and where the magic step from detailed design to programs could be demystified. We also applied the structuring ideas to develop formal accounts of the concept of software architecture.
Much of the work (though not all!) on MAL and temporal logics during the 90s neglected the deontic aspects of the language. In the last 2 years, I have again become interested in the topic because of theory required to underpin e-commerce, and, in particular, concepts such as trust, deception, contract negotiation and execution. There is also a strong connection with fault tolerance mechanisms and their logical modelling. Work on contrary to duty structures would appear to be relevant here.
During the 90s, I made a new contact at PUC in Rio, namely Armando Haeberer. With him I have worked on object oriented modelling techniques and business process modelling. We have also attempted to develop a framework for software engineering, based on the epistemological principles advocated by Carnap and his successors. The investigation was prompted by us asking ourselves questions like: How can we justify to colleagues that this object oriented design environment that we are proposing to build will be more effective than environment X? During the work, we have clarified a number of epistemological notions and developed explanations of the epistemological status of requirements specifications, the relationship between programs and designs, etc and provided scientifically sound definitions of many fuzzy concepts in software engineering.