Towards a proof method for Paradigm. (English) Zbl 1475.68184

Ábrahám, Erika (ed.) et al., Theory and practice of formal methods. Essays dedicated to Frank de Boer on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 9660, 242-260 (2016).
Summary: 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.
For the entire collection see [Zbl 1460.68002].


68Q60 Specification and verification (program logics, model checking, etc.)


Full Text: DOI