Taxonomy of Inconsistency Patterns in Multi-View Modelling
Case RCM05-4

Source

Wehrheim2005

Categories

C1 (primary); C3 (secondary)

Domain

model-driven development

formal multiview refinement

Views

dynamic protocol model A

refined protocol model C

Artefacts

send transition in A

prepare/transmit transitions in C

Quotes

"Sending is split into preparation and transmission. […] After a trace of C in which prepare has occured but transmit not, transmit may not be refused. There are no traces in C in which transmit occurs without a prior prepare."

"Has every behaviour of C a corresponding behaviour in A?"

Summary

A send transition is split into prepare and transmit in the protocol state machine, with extra ordering constraints needed to avoid spurious behaviour.

Cause: behavioural refinement introduces intermediate protocol states that must still correspond to one abstract transition.

As a result, without the extra constraints, the refined protocol can exhibit traces that the abstract protocol never allowed.

Taxonomy Categories

Evidence Map

---

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: March 2026.