View article

Scenarios and State Machines offer two complimentary views on the behavior of distributed systems. The former presents a bird’s eye view on objects interactions, whereas the latter describes the complete behavior of every object, thus being closer to implementation. Many algorithms translating scenarios to state machines have been devised. All these algorithms work at instance-level, ie for a fixed finite number of objects. Real-world object-oriented systems may contain arbitrarily many objects. 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.