  Stochastic models are widely used to verify whether systems satisfy their
reliability, performance and other nonfunctional requirements. However, the
validity of the verification depends on how accurately the parameters of these
models can be estimated using data from component unit testing, monitoring,
system logs, etc. When insufficient data are available, the models are affected
by epistemic parametric uncertainty, the verification results are inaccurate,
and any engineering decisions based on them may be invalid. To address these
problems, we introduce VERACITY, a tool-supported iterative approach for the
efficient and accurate verification of nonfunctional requirements under
epistemic parameter uncertainty. VERACITY integrates confidence-interval
quantitative verification with a new adaptive uncertainty reduction heuristic
that collects additional data about the parameters of the verified model by
unit-testing specific system components over a series of verification
iterations. VERACITY supports the quantitative verification of discrete-time
Markov chains, deciding which components are to be tested in each iteration
based on factors that include the sensitivity of the model to variations in the
parameters of different components, and the overheads (e.g., time or cost) of
unit-testing each of these components. We show the effectiveness and efficiency
of VERACITY by using it for the verification of the nonfunctional requirements
of a tele-assistance service-based system and an online shopping web
application.
