Probabilistic Verification of Architectural Software Models Using SoftArc and Prism
In this paper, the authors will describe the SoftArc approach. With the SoftArc approach it is possible to model and analyze safety-critical embedded and distributed systems that consist of both hard- and software. They are going to present the SoftArc modelling language, its syntax and semantics. The semantics of the SoftArc modelling language is defined in terms of stochastic reactive modules. They will show how important measures of interest for probabilistic dependability analysis like availability, unavailability, and survivability, can be analyzed.