• home
• current students
• graduate
• events

Presenter: Dr. Kousha Etessami - Bell Labs, Murray Hill, NJ - Faculty Applicant
Supervisor: R. Nigel Horspool, Chair, Department of Computer Science

Date: Thu, February 15, 2001
Time: 09:00:00 - 10:00:00
Place: Engineering Office Wing Building (EOW), Room #430

ABSTRACT

ABSTRACT:

In current model checking practice, a finite state machine is used to model each component of a concurrent system and the model checker's job is to detect whether the model satisfies some logical specification. To adequately model a component which itself consists of a sequential program containing multiple procedures that invoke each other, potentially recursively, it is less appropriate to use one monolithic finite state machine than it is to use one state machine for each procedure and allow state machines to invoke each other.

We introduce and study recursive state machines (RSMs) which formally model precisely this phenomenon. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can also be viewed as a visual formalism extending Statecharts-like hierarchical state machines, and they are related to various other models studied in the verification and program analysis communities.

A critical issue is whether model checking and state space analysis can be performed efficiently for such machines. Ordinary finite state model checking has a running time linear in the size of the aggregate model. We describe an algorithm for model checking recursive state machines that runs in linear time as long as certain parameters of the model remain bounded.

In this talk, I will set this work in the broader context of current research in verification, including recent efforts on tools to (semi automatically extract models directly from programs written in modern imperative languages.

(This talk describes joint work with: R. Alur (U. Penn) and M. Yannakakis (Bell Labs))