A Rewriting Logic Semantics and Statistical Analysis for Probabilistic Event-B

TL;DR

This paper introduces a rewriting logic semantics for probabilistic Event-B, enabling automatic simulation and verification of probabilistic systems with statistical testing capabilities.

Contribution

It provides a formal semantics for probabilistic Event-B, capturing key probabilistic behaviors and enabling automated simulation and statistical analysis.

Findings

Semantic framework is fully executable in PMaude.

Supports probabilistic assignments, parameters, and concurrency.

Facilitates statistical testing of probabilistic models.

Abstract

Probabilistic specifications are fast gaining ground as a tool for statistical modeling of probabilistic systems. One of the main goals of formal methods in this domain is to ensure that specific behavior is present or absent in the system, up to a certain confidence threshold, regardless of the way it operates amid uncertain information. This paper presents a rewriting logic semantics for a probabilistic extension of Event-B, a proof-based formal method for discrete systems modeling. The proposed semantics adequately captures the three sources of probabilistic behavior, namely, probabilistic assignments, parameters, and concurrency. Hence, simulation and probabilistic temporal verification become automatically available for probabilistic Event-B models. The approach takes as input a probabilistic Event-B specification, and outputs a probabilistic rewrite theory that is fully executable in PMaude and can be statistically tested against quantitative metrics. The approach is illustrated with examples in the paper.