Speaker: Dr. Yuri Gurevich, Microsoft Research
2:30 pm, Thursday, April 17, 2003
Halpern Centre, Simon Fraser University, Burnaby, BC
This talk is directed to computer scientists, computer engineers and mathematicians. Please visit the PIMS site for a Real broadcast of Dr. Gurevich's lecture.

Title:
Executable Specifications: The Abstract State Machine Approach

Abstract
To specify software means to describe it one way or another. We are interested in specifications taht are precise, high level and executable. Some people think that executable specifications will change the way software is designed, developed, tested and documented. Our opinion is based on the theory of abstract state machines, extensive international experimentation with ASM, and the applied ASM work of the group on Foundations of Software Engineering at Microsoft Research.

Contrary to natural sciences, computer science is about artificial reality, about computer systems. Mathematically speaking, what is a computer system? A computer system may have many levels of abstraction. Fix such a level. The ASM theroy tells us that there is an abstract state machine that behaviorally, is identical to our system on the chosen abstract level. The specification language Asml, developed by the FSE group, makes writing ASM models practical. Our tools allow the developers (more and more) to experiment with their design, validate it and enforce it. The tools allow testers to be involved earlier in the software development cycle and empower them to test the intended functionality of software (and not only its robustness).