Abstrakt
Populární přístup ke kompoziční verifikaci komponentových aplikací je založen na principu assume-guarantee (domněnka-záruka), kde domněnka modeluje chování prostředí pro každou komponentu. Realistické komponentové aplikace často zahrnují složité vzory komunikace jako callbacky a autonomní aktivity, které musejí být brány v úvahu modelem chování prostředí.
Obecně, takové vzory mohou být přesně modelovány pouze formalismem, který (i) podporuje nezávislé atomické události pro volání metod a návraty z metod a (ii) dovoluje specifikaci explicitních proložení událostí na poskytovaných a požadovaných rozhraních komponenty - formalismus protokolů chování splňuje tyto požadavky. Tento článek se pokouší zodpovědět otázku, jestli model zahrnující pouze události na poskytovaných rozhraních (volací protokol) může být korektní při nějakých omezeních na chování komponent.
Hlavním přínosem jsou omezení na proložení událostí a zhodnocení navržených omezení na realistických komponentových aplikacích.