We present a choreographic framework for modelling and analysing concurrent probabilistic systems based on the PRISM model-checker. This is achieved through the development of a choreography language, which is a specification language that allows to describe the desired interactions within a concurrent system from a global viewpoint. Using choreographies gives a clear and complete view of system interactions, making it easier to understand the process flow and identify potential errors, which helps ensure correct execution and improves system reliability. We equip our language with a probabilistic semantics and then define a formal encoding into the PRISM language and discuss its correctness. Properties of programs written in our choreographic language can be model-checked by the PRISM model-checker via their translation into the PRISM language. Finally, we implement a compiler for our language and demonstrate its practical applicability via examples drawn from the use cases featured in the PRISM website.

翻译：我们提出了一种基于PRISM模型检测器的并发概率系统建模与分析编排框架。该框架通过开发一种编排语言实现，这是一种规范语言，允许从全局视角描述并发系统中期望的交互行为。使用编排语言能够清晰完整地呈现系统交互，使流程更易于理解并有助于识别潜在错误，从而确保正确执行并提升系统可靠性。我们为该语言赋予概率语义，随后定义其到PRISM语言的正式编码并论证其正确性。通过将用本编排语言编写的程序翻译为PRISM语言，可利用PRISM模型检测器对其进行性质验证。最后，我们实现了该语言的编译器，并通过PRISM官网用例库中的实例展示了其实际适用性。