INTERNATIONAL
LOGIC AND COMPUTER SCIENCE
SEMESTER AT TEL-AVIV

Guest Lecture

Yuri Gurevich, Microsoft Research

Wednesday, April 28, 2004, 16:00-17:30
Kaplun #324

Executable Specifications: The Abstract State Machine Approach

Some people think that executable specification is a contradiction in
terms.  We 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, international
experimentation with ASMs, and the applied ASM work of the group on
Foundations of Software Engineering in Microsoft Research.

Contrary to natural sciences, computer science is primarily about
artificial reality, about computer systems.  Mathematically speaking, what
is a computer system?  A computer system may have many meaningful levels
of abstraction.  Fix such a level.  The ASM theory tells us that there is
an abstract state machine that, behaviorally, is identical to our system
on the chosen abstraction 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).

Bio: Yuri Gurevich is Sr. Researcher at Microsoft Research in Redmond, WA.  He
is also Professor Emeritus at the University of Michigan, ACM Fellow,
Guggenheim Fellow, and Dr. Honoris Causa of Limburg University in Belgium.