A Graphical Notation for Probabilistic Specifications

ABSTRACT. Nowadays formal methods represent a powerful but in practice not well supported way for verification. One reason among others for this is that such methods are often conceived of being too theoretical, can likely be misunderstood by non-experts, and notations are therefore misapplied.

For example to specify formal specifications, complex logics are state-of-the-art, especially for probabilistic verification properties. It is not only that users are unable to construct correct specifications but they also miss to understand what is meant by the verification results based on the specification.

In this paper we address this problem and endorse the usage of a graphical notation to construct such specification properties, especially probabilistic ones. We present how such a notation may look and emphasize that one single notation is sufficient to solve both lack of comprehensibility of the specification as well as of the verification results. Moreover, we extract some future research directions.