In 1989 I received a B.Sc. (Eng.) degree in Engineering Mathematics from Queen's University in Kingston, Ontario and in 1992 and 1997, respectively, I was awarded M.A.Sc. and Ph.D. degrees from the Systems Control Group, Department of Electrical and Computer Engineering at the University of Toronto. During the course of my doctoral studies I held contract positions as a real-time simulator consultant at AlliedSignal Aerospace Canada Ltd. (now a part of Honeywell) and as an internet consultant at QuickLaw Ltd.
Upon completing my doctorate, I worked for a year and a half at Ontario Hydro (now Ontario Power Generation) as a real-time software verification consultant on the Darlington Nuclear Generating Station Shutdown Systems Redesign project. Since August of 1998 I have been an Assistant Professor in the Department of Computing and Software at McMaster University where I am helping to develop and teach the Software Engineering program.
My research interests include supervisory control of discrete event systems and a broad range of formal methods for safety critical real-time systems including equivalence verification, model-checking and theorem proving techniques. One of my most active research areas is what I would loosely call computer aided inspection of software. As part of my research efforts in this area I co-organized the Workshop on Inspection in Software Engineering that was one of the satellite workshops of CAV'01. I am a member of the MathScheme project which, in the words of our fearless project leader, will seek to "integrate and generalize computer theorem proving and computer algebra." My role in the MathScheme project will be to develop software verification applications and examples on top of the micro-kernel. My interest in Mathematical Knowledge Management stems from the fact that although I have successfully used model-checkers and theorem provers to solve real-time control software verification problems, I am often frustrated by these tools non-existent or rudimentary algebraic abilities. I believe that that new mathematical tools are needed to help software engineers answer that all important question: "Does this real-time control system do what we want?"
I am mainly interested in Mathematical Knowledge Management (MKM) Systems from the Software Engineer as end user point of view. To be truly useful I believe that such systems will have to incorporate these three areas of research in mechanized mathematics:
The development of software for safety critical control systems represents an engineering application domain that would benefit from a tighter integration of these tools. Currently, a computer algebra system might be used in the controller synthesis of a mixed discrete/continuous "Hybrid" control system, model-checking can be applied to verify properties of system's discrete dynamics and theorem proving can be used to help verify the controller software implementation.
While each of these types of mathematical tools have been applied in isolation to the development and verification of control systems software, all are needed to help guarantee the overall correctness of the system. Further, in reasoning about the correctness of control software, problems arise that would be more easily solved using a combination of these tools. While many of these problems may be "junk theorems" (i.e., not mathematically interesting or even necessarily extremely difficult to solve), they are numerous, often tedious, but absolutely necessary to verify it an engineer wants to be sure the control system will operate safely.
This leads to two other challenges that need to be addressed by MKM Systems:
A significant challenge will be not only insuring that computer algebraic manipulations, model-checking decision procedures and theorem proving operations that compose a MKM system are soundly implemented, but also guaranteeing that soundness bugs are not injected into the system by the way that the theorem proving, computer algebra and model-checking components interact. Implicit assumptions about semantics or implementation details by the different developers working on the main system components is a cause for concern.
While I have had some limited success teaching both undergraduate and graduate software engineering and/or computer science students how to use theorem provers and model-checkers, it requires significant effort for the students to overcome the steep learning curve associated with these tools. Perhaps one of the most daunting tasks faced by developers of MKM Tools will be to deliver a tool that is usable by the non-expert. I believe that one of the most important ways of achieving usability of these systems will be through applying these tools to application domains such as real-time control systems software development and verification.
A list of some of my publications, including links to download papers, is available from http://www.cas.mcmaster.ca/~lawford/papers/.