The paper describes two perspectives on a verification approach for Paradigm, a coordination modeling language specifying an architecture in terms of components and their collaborations. One perspective concentrates on a single collaboration: per collaboration, properties can be derived through a small set of proof rules. The other perspective concentrates on dynamic dependencies between collaborations: guided by the architecture and driven by shared components behavioral properties of the complete model can be established. Two Paradigm models, a parallel assignment and a linear pipeline of workers and buffers, illustrate the approach.
|Title of host publication||Theory and practice of formal methods: essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday|
|Editors||E. Abraham, M.M. Bonsangue, E.B. Johnsen|
|Place of Publication||Berlin|
|Number of pages||19|
|Edition||Lecture Notes in Computer Science|
|Publication status||Published - 2016|
|Name||Lecture notes in computer science |