Inventors:
Rajeev Alur - Ardmore PA
Kousha Etessami - New York NY
Mihalis Yannakakis - Summit NJ
Assignee:
Lucent Technologies Inc. - Murray Hill NJ
International Classification:
G06F 954
US Classification:
709318, 703 17, 706 10, 345440
Abstract:
A system and method for determining whether a set of message sequence charts (MSCs) is realizable or safely realizable in an implementation is provided. The determination is made by analyzing the set of MSCs for the existence of unspecified, implied MSCs. If the set of MSCs can be realized in a deadlock-free automaton, then the set of MSCs is safely realizable. If the set of MSCs is realizable (no implied MSCs exist), a state machine can be synthesized from the set of MSCs. If the set of MSCs is not realizable, then implied, unspecified (partial) MSCs are produced. Also, given an undesirable MSC, the system determines whether the set of required MSCs implies the given undesired MSC.