Ulysses: Protocol Synthesis from Scenario-based Specifications

Alvise Bonivento and Marco Sgroi
(Professor Alberto L. Sangiovanni-Vincentelli)

The design of protocols, i.e., the set of rules that define how the communication among two or more components of a distributed system takes place, requires the use of formal techniques and tools to obtain a correct and efficient implementation. Ulysses is a new approach for protocol synthesis from scenario-based specifications. It allows the designer to specify sequences of interactions called scenarios using message sequence nets (MSNs), a model that includes message sequence charts and explicitly shows the relations of ordering concurrency or conflict among multiple MSCs. It uses Petri Nets (PNs) as an underlying model to formally define the semantics of MSNs and to specify the internal protocol behavior. A covering procedure that uses common case patterns and derives a PN model consistent with the original MSN is defined. Independently-specified scenarios are then composed to derive a minimum cost implementation.

Send mail to the author : (sgroi@eecs.berkeley.edu)

Edit this abstract