Towards a proof method for Paradigm
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.
Groenewegen, L.P.J, Kuiper, R, & de Vink, E.P. (2016). Towards a proof method for Paradigm. doi:10.1007/978-3-319-30734-3_17