From Interaction Diagrams to State Machines: Moving to Class-Level

Scenarios and State Machines offer two complementary views on the behavior of distributed systems. The former presents a bird's eye view on ob jects interactions, whereas the latter describes the complete behavior of every ob ject, thus being closer to implementation. Many algorithms translating scenarios to state machines have been devised. All these algorithms work at instance-level, i.e. for a fixed finite number of ob jects. Real-world ob ject-oriented systems may contain arbitrarily many ob jects. Modeling languages and synthesis algorithms need to be adapted to this situation. We propose a simple and elegant extension of State Machines and Interaction Diagrams, that adds universal/existential quantifiers. This makes it possible to describe protocols such as "when some observer detects an event, it notifies all registered clients". The problem we want to solve is precisely defined and an algorithmic solution is given and proven correct. Our synthesis algorithm is similar to state of the art approaches but adds a novel instantiation step to cope with quantifiers.