  The BPMN 2.0 standard is a widely used semi-formal notation to model
distributed information systems from different perspectives. The standard makes
available a set of diagrams to represent such perspectives. Choreography
diagrams represent global constraints concerning the interactions among system
components without exposing their internal structure. Collaboration diagrams
instead permit to depict the internal behaviour of a component, also referred
as process, when integrated with others so to represent a possible
implementation of the distributed system.
  This paper proposes a design methodology and a formal framework for checking
conformance of choreographies against collaborations. In particular, the paper
presents a direct formal operational semantics for both BPMN choreography and
collaboration diagrams. Conformance aspects are proposed through two relations
defined on top of the defined semantics. The approach benefits from the
availability of a tool we have developed, named C4, that permits to experiment
the theoretical framework in practical contexts. The objective here is to make
the exploited formal methods transparent to system designers, thus fostering a
wider adoption by practitioners.
