In my view, development tools, and in particular specification languages, play a central role in the problem of developing human-computer systems. Note that specification languages include notations that perhaps not everyone will consider as being languages: in particular, abstract or diagrammatic notations, such as dataflow and class diagrams, and special shorthands added to another language, such as pattern matching facilities.
Another approach I might have chosen is the development of theories: for example, Gricean models, DRT, dialogue grammars, modality theory, cognitive ergonomics, and semiotics. Such theories provide heuristics for systems design. In the ideal case, such theories should provide the necessary a priori insight that enables one to properly specify a human-computer system (and in particular, a multimodal or natural language dialogue system) without too much re-design. However, after some research, I came to the conclusion that existing theories can hardly be said to guarantee such insight. It may be said that there is a long road from theory and conception of a system to an actual working version: there is a large amount of details to be dealt with along the way. For example, there are few dialogue systems directly based on Gricean theory or other rational / intentional / plan-based theories of dialogue. These theories are very hard to encode directly into an executable form, or any other formal specification with a sufficiently level of detail to make it implementable without having to resolve further details. This means that the application and communication of insights based on some specific theory remains highly qualitative and intuitive. This makes it very hard to assert proper control over systems development using theory alone. It is, in fact, already hard enough to find out whether a system built using a theory is better than a system built without it.
Complementary to theories, the general development approach that is usually used is an evolutionary one of observation and experimentation (or trial and error): observe what people do, then hard-code this into a computer system, then observe what people do with the system, then improve the system, etc. This has to be done over and over again for every new system that is built. This evolutionary concept is found in both dialogue systems (for example, the Wizard of Oz method) and HCI (mock-ups and prototyping). While theory may be necessary for being able to build a system that works at all, it is very likely that, even more so than in software engineering in general, an evolutionary approach will remain a necessary evil. It is in fact likely to become more important as human-computer systems become more complex.
So, my conclusion is that, as much as are theories, tools are needed that enable this evolution to proceed more quickly and smoothly. This is where my focus on specification languages comes in: it facilitates the `trial' part of the trial and error process. A specification language smoothes the road between conception and implementation: it should be possible to use it extensively to document and communicate. A specification framework could be further extended to include standard (software) libraries and design `patterns': these would be `crystallisations' of the most directly applicable parts of existing theory, though this would bind the framework to a specific theory. The `error' part (evaluation) is a subject of future research, and will probably fall outside the scope of my project.
Preferably, a specification language is executable, which implies that it is formal. For the sake of dialogue and usability evaluation, it should actually be akin to a programming language, enabling prototypes to be built, though perhaps these need not be quite suitable as `final versions' of the system being specified. Though it is of course possible that a specification language is complemented by other, formal or informal, executable or non-executable, languages, it is important that the information described in the different specifications is actually consistent. However, it is hard to keep information consistent: some people think that even keeping documentation consistent with a program is too hard, and want to do away with documentation altogether. This means that the choice of `central' language--in other words, the one that is the most directly related to the system being built--will have a great impact on the development process.
Our own Schisma dialogue manager was implemented directly in Java. When one looks at the code, one finds various kinds of `hackery' in it, such as a complex context resolving scheme, and a specific action sequencing and error bailout scheme. It is not `mere' hackery: such seeming idiosynchacies are needed to make the system work. The specification is not easy to read, and people have been reluctant to take a close look at the code. Of course, there was no time to write documentation either. Nobody as yet has attempted a rewrite, even though some evaluation results are now available, as well as a new parser. Possibly, the dialogue manager will be replaced eventually, and much of the knowledge in the old system may be lost. Much the same goes for the graphical part of the dialogue system. Possibly, a different choice of specification language may have improved this situation.
Even though there is a great variety of specification languages, the first step towards a development framework should include a relatively complete review of existing specification languages. At the same time, determining whether a language is suitable or not is a subtle problem. Particularly subtle is the usability of a language, in the psychology of programming sense: it depends on the goals that the users of the language have, and the tasks that they go through to achieve them. Any evaluation of specification languages will probably remain highly qualitative, and detailed evaluation of a language for use with a new application domain will at least require trying to specify some systems using it.
Complementary to proof, simulation (`testing') is often used. A number of example runs of a (possibly non-abstract version) of the system are made, which, again, may increase confidence of the correctness of the system.
Programming languages are good at description and simulation: you can describe the whole system (although not always in a very easily readable form), and it can be executed immediately. While it would be fairly straightforward to automatically translate large parts of a program into logic or process algebra, the resulting specification is not likely to be tractable for proof.
However, many people using the term `formal methods' primarily indicate proof. Proofs are often done using a separate language. The specifications that one starts with in these languages do not always enable simulation: they are so far away from actual implementation that implementations cannot be generated automatically or without requiring choices. Proof may be computer-aided (theorem provers) or automated (model checkers). This does not mean, however, that proof always requires the use of a separate language. Some languages actually enable both proof and simulation. For example, Promela, while actually a model checking language, looks a lot like a traditional programming language, and might be used as one. In practice, it is likely that some kinds of proof will require a separate language.
Yet, what I've seen is that many of the `formal specifications' in the literature (for example, many of the Z specifications and `intentional logic' specifications) are only descriptions. While the language being used happens to be one that is particularly suitable for proof, there's little proof being done. The languages aren't executable either. In my opinion, such use of formal language is somewhat questionable, and is not actually what I'd call a formal method: one can describe a lot of things, but there's no correctness feedback at all. One might as well be using natural language.
I will give a short account of my idea of a good specification language and its role in development here. Typically for human-computer systems, an analysis or requirements phase is done first. This phase typically uses informal specification languages, such as natural language and pictures. Soon after this, though, relatively concrete implementations of the system emerge. It would save time if these early implementations are already written in the same language that is used throughout development. The capabilities of the language for description and simulation are obviously important here.
Especially for complex concurrent systems, proof may be useful as well. Describing a system in the right manner facilitates proof, both by aiding intuition and by making some computer-aided proof methods more feasible. While reading the specification, a designer may get an intuition about weak spots in the system, and may decide to do a proof. Then, part of the system is selected (abstraction), and secondary properties specified or formalised, and the proof is done. It is likely that getting the proof process right requires some iteration and `de-bugging'. The results of the proof should be documented separately.
To be continued
The first attempt was done using the process algebra CSP, together with my advisor Job Zwiers. This included writing system and task models, and a small parser and execution engine to generate prototypes out of CSP specifications. This part of my research resulted in a workshop paper. CSP is good for specifying both composition and behaviour of an interactive system with multiple components, but some weaknesses are also apparent: it is not good for specifying systems with a dynamical number of components, and it is not really suitable for specifying the behaviour of dialogue managers to a reasonable level of detail. Furthermore, it is probably not possible to use a CSP framework all the way to the final version of the system.
The need for more expressive power has led us to consider several other description languages, including object-based extensions to process algebra, and some of the existing `agent-based' models. Meanwhile, further practical engineering issues were revealed in discussions w.r.t. plans to extend the VMC to include other agents and make it into a multi-user system. As an answer to all this, I came up with a update notification (or publisher-subscriber) model, based on existing interactor and agent models. This part of my research is described in a technical report. Also contained in this report is a further refined evaluation of process algebras.
In this report, I have also tried to further frame my research topic. In particular, I have argued that the most promising specification languages are process algebras, production rule systems, and dataflow / interactor / publisher-subscriber models. It is likely that these will become the main focus of the rest of my project. I have proceeded by writing some software: an engine for the update notification model I proposed, with a multi-user `mini VMC' application. Since this model fits neatly within production rule systems (which are conceptually close to event handling loops, and also deal with sets) I am now working on a production rule based control flow language to go with the model (possibly making use of the JEOPS engine). Such a language would play the same role as CSP in the previous prototype generation model: the production rules define the sequencing of events and function calls, enabling the control flow of a module to be specified in a concise and insightful manner, while still allowing the functionality of existing programming libraries to be used. The combination of these two models should provide the necessary expressive power missing in CSP.
This software may be further extended to evolve into a ready-to-use development toolkit. It should also be equipped with some standard libraries and templates selected from the literature. The resulting toolkit should enable multimodal dialogue systems and multi-agent / multi-user virtual environments to be specified, prototyped, and possibly verified, easily. Next to producing prototypes, the framework should preferably support development of the system all the way to the final version. At first, a rough prototype may be built and tested using the built-in facilities only, and later, parts of the system may be incrementally replaced by more refined, and probably highly application-specific, components.
However, it is not entirely clear just how far the toolkit will help towards specification of a final product in the near future. While it should in the short term be possible to add, for example, speech recognition and generation to an application, producing fancy animations has proven hard, particularly because the underlying software libraries are still not very well developed. Another problem is efficiency (for example, network and database query efficiency), which may require years, and different research disciplines, to improve.
The original technique, which was based entirely on process algebra, is hereby left behind. Nevertheless, the resulting assessments (and experience!) of process algebras may yet prove useful. Process algebras may still be incorporated in the toolkit, or used as a complementary language as part of a methodology. In particular, as rumours go, large production rule systems are hard to maintain, and some kind of protocol checking or model checking may prove to be a great help. Firstly though, I think that a more detailed `psychology of programming' assessment of production rule languages is in order at this point. This would be very interesting, because, as far as I know, this has not really been done before.