Department of Computer Science and Engineering
Michigan State University
3115 Engineering Building
East Lansing, MI 48824-1226
Phone: 517-353-4387
Fax: 517-432-1061
Email: ldillon@cse.msu.edu
URL: http://www.cse.msu.edu/~ldillon
Laura (Laurie) K. Dillon received the Ph.D. degree in Computer Science from the University of Massachusetts at Amherst (UMASS) in 1984. She subsequently spent a year on the faculty at UMASS and twelve years on the faculty at the University of California, Santa Barbara (UCSB). In 1997, she moved to Michigan State University (MSU), where she is now a full professor.
Laurie's research interests center on formal methods for specification and analysis of concurrent software systems, programming languages, and software engineering. She is active in the software engineering community, having served over the years in various editorial capacities, and on numerous program committees, funding panels, and professional advisory committees. Most recently, she was a program co-chair of the 2003 International Conference on Software Engineering, and she is currently a member of the Executive Committee of the ACM Special Interest Group in Software Engineering. She is a member of ACM, IEEE, AAUW, WEPAN, and CPSR.
Can you afford to release software that could bring down the store, leave phone calls hanging, or route two airplanes into the same airspace? Can you prevent software bugs that "should be" caught in testing from eluding your testing team and coming back to bite you?
Testing is not capable of proving that a system behaves correctly under all circumstances. However, it remains the most cost-effective means of demonstrating system dependability, and as such it is a crucial software development activity. Yet the typical testing process is such a human intensive activity that it is by nature error-prone and unproductive. Put simply, testing is all too often inadequately done.
The automation and formalization of testing techniques can enhance productivity of software developers and reduce errors in the development process. Formalization entails the use of formal methods in specifying and reasoning about product requirements and also in defining requirements of the testing process.
This talk will describe an application to testing of a specific formal method related to temporal logic. (A temporal logic is a formal logic that has been extended with a notion of ordering in time. Classical logic does not include such a notion, which is important for expressing requirements of many embedded, real-time systems---e.g. phone switches, avionics.)
The talk will describe a logic in which to specify temporal properties of real-time systems, called Graphical Interval Logic (GIL), as well as a method for constructing "oracles" from GIL specifications. GIL oracles check for temporal faults in test executions, ensuring that the testing team does not overlook executions that exhibit subtle timing and ordering faults. The visually intuitive representation of GIL specifications makes them easier to develop and to understand than specifications written in more traditional temporal logics. Additionally, when a test execution violates a GIL specification, the oracle provides information about a failure. This information can be displayed visually, together with the execution, to help the system developer see where in the execution a failure was detected and the nature of the failure.
The talk describes a toolset for specification and verification of concurrent systems based on Graphical Interval Logic. Specifications in the logic have an intuitive visual representation that resembles the timing diagrams drawn by hardware and software engineers. The toolset includes a visual editor for drawing graphical formula on a workstation display, an automated proof checker for certifying the validity of proofs, and a simple proof management and database system. All user interaction is through the visual interface provided by the editor. An example is presented to illustrate the use of the tools in reasoning about the correctness of a system.
Automatic-verification capability tends to be packaged into stand-alone tools, as opposed to components that are easily integrated into a larger software-development environment. Such packaging complicates integration because it involves translating internal representations into a form compatible with the stand-alone tool. By contrast, lightweight-analysis components package analysis capability in a form that does not require such a translation.
The Amalia framework generates lightweight components that automate the analysis of operational specifications and designs. A key concept is the step analyzer, which enables Amalia to automatically tailor high-level analyses, such as behavior simulation and model checking, to different specification languages and representations. A step analyzer uses a new abstraction, called an inference graph, for the analysis. The nodes of an inference graph directly reify the rules in an operational semantics, enabling Amalia to automatically generate a step analyzer from an operational description of a notation's semantics.
This talk will provide an overview of the approach to producing lightweight tools used in Amalia. It will describe inference graphs and provide an example using Lotos.