{Modeling and Verification of Business Processes and Choreographies in ALP}