CSPm models for the ATM case study
- 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.
Document Type: | Conference Object |
---|---|
Language: | English |
Author: | Andreas V. Hense |
Parent Title (English): | S-BPM ONE '15. Proceedings of the 7th International Conference on Subject-Oriented Business Process Management. April, 23-24, 2015 in Kiel, Germany |
Article Number: | 20 |
First Page: | 1 |
Last Page: | 7 |
ISBN: | 978-1-4503-3312-2 |
DOI: | https://doi.org/10.1145/2723839.2723866 |
Publisher: | Association for Computing Machinery |
Place of publication: | New York, NY, United States |
Date of first publication: | 2015/04/23 |
Copyright: | Copyright 2015 ACM. Abstracting with credit is permitted. |
Departments, institutes and facilities: | Fachbereich Informatik |
Dewey Decimal Classification (DDC): | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik |
Entry in this database: | 2015/05/26 |