July 1996
Proceedings of the BCS-FACS 7th Refinement Workshop (RW)
BCS-FACS 7th Refinement Workshop
3-5 July 1996
B AMN, Object calculus, concurrent specification, safety and liveness properties
This paper outlines an approach to extending B AMN to support concurrent specification, using a combination of linear temporal logic and Ada style task definitions. The extension is applied to the “production cell” case study.
This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/