@inproceedings{Hense2015, author = {Andreas V. Hense}, title = {CSPm models for the ATM case study}, series = {S-BPM ONE '15. Proceedings of the 7th International Conference on Subject-Oriented Business Process Management. April, 23-24, 2015 in Kiel, Germany}, publisher = {Association for Computing Machinery}, address = {New York, NY, United States}, isbn = {978-1-4503-3312-2}, doi = {10.1145/2723839.2723866}, pages = {1 -- 7}, year = {2015}, abstract = {Communicating Sequential Processes (CSP) [7] is a calculus for concurrent systems that has been the basis of subject-oriented business process management (S-BPM) [4]. We use CSPm -- a machine readable dialect of CSP -- to create a sequence of models for a case study on an \"Automated Teller Machine\" [1]. We use the refinement checker FDR2 to prove that certain models are correct implementations of specifications.}, language = {en} }