Checking consistency of SDL+MSC specifications

		    Deepak D'Souza,
	Indian Institute of Science, Bangalore.

We consider the problem of checking whether a distributed
system described in SDL is consistent with a set of MSCs that
constrain the interaction between the processes.  In general,
the MSC constraints may be both positive and negative.  The
system should execute all the positive scenarios ``sensibly''.
On the other hand, the negative MSCs rule out some interactions
as illegal.  We would then like to verify that all the
remaining legal interactions satisfy a desired global property,
specified in linear-time temporal logic.  We outline an
approach to solve this problem using Spin, building in a
modular way on existing tools.

This is joint work with Madhavan Mukund, CMI Chennai.