Process Top level message sequence chart Partners The actors in the scenarios Containers specify variables for message data Correlationsets dependencies between messages Flow concurrent message transitions Assign messages that require data storage Switch test and branch conditions Sequence sequential execution of activities While scenario iterations Receive messages input from services Reply messages sent back to services

<process name="marketplace"       targetNamespace = "urn:MPService"       xmlns:tns="urn:MPService"..>      <flow name="MarketplaceAgree">      <receive partner="seller"               portType="tns:sellerPT"               operation="submit"               container="sellerAgree"               createInstance="yes"               name="SellerAgree">       </receive>       <receive partner="buyer"               portType="tns:buyerPT"               operation="submit"               container="buyerAgree"               createInstance="yes"               name="BuyerAgree">       </receive>       </flow> </process>

Overview of model checking of BPELS @ Model-based Verification of Web Service Compositions Howard Foster, Sebastian Uchitel, Jeff Magee, Jeff Kramer Department of Computing, Imperial College London, UK, 2002. doi=10.1.1.5.3846