Penn Arts & Sciences Logo

Logic and Computation Seminar

Monday, October 21, 2002 - 4:30pm

Rajeev Alur

University of Pennsylvania

Location

University of Pennsylvania

DRL 4C8

Note venue change.

Scenario-based specifications such as message sequence charts offer an intuitive and visual way of describing design requirements. Such specifications focus on message exchanges among communicating entities in distributed software systems, and form an integral part of modern software design environments such as UML. Requirements expressed using MSCs have been given formal semantics, and hence, can be subjected to analysis to reveal inconsistencies. This talk surveys algorithms for a variety of such analyses including detecting race conditions, inferring implied scenarios, and model checking with respect to temporal logic requirements.