View article

Estimation of quantitative properties of software models can provide useful insights early in the development process. However, computational complexity of estimating reliability or service-level metrics such as mean time to first failure (MTTF) or turnaround time (TAT) can be prohibitive both in time, space and precision. A promising approach to tackling this complexity is to compute lower bounds to these measures, based on partial explorations of the system under analysis:(i) Model simulation to obtain samples of system behaviour;(ii) Invariant inference from samples; and (iii) exhaustive model checking of the submodel defined by the invariant. However, existing work on quantitative analysis using partial explorations is limited to deterministic models (which cannot be easily simulated) and MTTF properties.