[HS12] Luke Herbert and Robin Sharp. Using stochastic model checking to provision complex business services. In Proc. 14th International IEEE Symposium on High-Assurance Systems Engineering (HASE'12), pages 98-105, IEEE. 2012. [Translates a subset of the Business Process Modelling and Notation (BPMN) language into PRISM, to allow probabilistic model checking of business workflows. Illustrated on a medical case study.]