|
The original motivations for the Omnibus project came from my experiences in a programming job that I had in the late 1990s. Run-time errors in the products that we were releasing were a source of tremendous distress to me and I would go to fairly extreme lengths to try to remove them. I believed that these errors were partly products of the development and testing techniques we were using. I was sure we could do better. This led me to start investigating Mathematical techniques for producing reliable software in December 2000.
In early 2001, I discussed my ideas with Dr Clark who referred me to the works of Meyer and Dijkstra. Later that semester I wrote a report presenting a first version of the assertion-based Omnibus language, along with an automatable heuristic theorem proving strategy. I was interested in how the approach could be used to avoid common programming errors like null pointer exceptions and array index out of bounds exceptions. The report also had sections on varying the level of analysis, component reuse and the importance of IDE-support, ideas that remain at the heart of the Omnibus project to this day.
I spent the following academic year at the University of California, Santa Barbara via the Education Abroad Programme. Whilst there, I got the opportunity to take a graduate level class on Formal Specification and Verification given by Professor Kemmerer and carry out a research project under the supervision of Professor Bultan, to survey the state-of-the-art tools including the original ESC/Java and JML. My final report argued that runtime-assertion checking, extended static checking and full formal verification could all be supported for a single language and mentioned that JML was the closest to achieving this, at the time supporting run-time assertion checking and full formal verification. In the Formal Specification and Verification class I was introduced to Symbolic Execution and wrote a prototype Object-based Symbolic Executor called Joose.
I was fortunate enough to be offered the chance to continue my work over the summer at Stirling with Dr Maharaj and this time helped lay the foundation for the Omnibus project that was now to be my dissertation. During the year I managed to produce a first version of the Omnibus language along with a tool to translate it to Java and a 339-page dissertation of over 90,000 words.
My main achievement of the first year of the Ph.D. was to develop a first version of the IDE for the language. The tool incorporated basic project and file management facilities, a type checker, a documentation generater and a Java code generation facility. I also developed schemes for the translation of Omnibus specifications to the logics of the Simplify and PVS provers and wrote a first draft of a textbook on how to write specifications using the language.
During the second year of my Ph.D., I implemented interactive and automated verifiers by automating the translation of Omnibus specifications to the logics of the Simplify and PVS provers. I also oversaw a successful honours project on applying Omnibus which developed a number of case studies and wrote a number of papers.
|
