Abstract
This paper discusses verification and optimization of complex systems with respect to a set of specifications under stochastic parameter variations. We introduce a simulation-based statistically sound model inference approach that considers systems whose responses depend on a few design parameters and many stochastic parameters. The technique iteratively searches over the space of design parameters by alternating between verification and optimization phases. The verification phase uses statistical model checking to check if the model using the current design parameters satisfies the specifications. Failing this, we seek new values of the design parameters for which statistical verification could potentially succeed. This is achieved through repeated simulations for various values of the design and stochastic parameters, and quantile regression to construct a model that predicts the spread of the responses as a function of the design parameters. The resulting model is used to select a new set of values for the design parameters. We evaluate this approach over several benchmark examples. In each case, the performance is improved significantly compared to the nominal design.
This work was supported by the US National Science Foundation (NSF) through grants CNS 1016994 and CCF 1320069. All opinions expressed are those of the authors, and not necessarily of the NSF.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
LTSpice: A high performance SPICE simulator, schematic capture and waveform viewer, http://www.linear.com/designtools/software/
Ben-Tal, A., Nemirovski, A.: Robust convex optimization. Mathematics of Operations Research 23(4), 769–805 (1998)
Bernardinis, F.D., Jordan, M.I., Sangiovanni-Vincentelli, A.: Support vector machines for analog circuit performance representation. In: DAC, pp. 964–969 (2003)
Campi, M.C., Garatti, S., Prandini, M.: The scenario approach for systems and control design. Annual Reviews in Control 33(2), 149–157 (2009)
Dalla-Man, C., Rizza, R., Cobelli, C.: Meal simulation model of the glucose-insulin system. IEEE Transactions on Biomedical Engineering 54(10), 1740–1749 (2007)
Doostan, A., Iaccarino, G.: A least-squares approximation of partial differential equations with high-dimensional random inputs. Journal of Computational Physics 228(12), 4332–4345 (2009)
Ellen, C., Gerwinn, S., Fränzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains (2014), to appear in a special issue on Statistical Model Checking
Henriques, D., Martins, J., Zuliani, P., Platzer, A., Clarke, E.: Statistical model checking for markov decision processes. In: QEST 2012 (2012)
Jha, S.K., Datta, R., Langmead, C., Jha, S., Sassano, E.: Synthesis of insulin pump controllers from safety specifications using bayesian model validation. In: Proceedings of 10th Asia Pacific Bioinformatics Conference, APBC (2012)
Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)
Kass, R.E., Raftery, A.E.: Bayes factors. Journal of the American Statistical Association 90(430), 774–795 (1995)
Koenker, R.: Quantile regression, vol. 38. Cambridge University Press (2005)
Lagoa, C.M., Dabbene, F., Tempo, R.: Hard bounds on the probability of performance with application to circuit analysis. IEEE Transactions on Circuits and Systems 55(10), 3178–3187 (2008)
Li, X.: Finding deterministic solution from underdetermined equation: large-scale performance variability modeling of analog/RF circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 29(11), 1661–1668 (2010)
Mitev, A., Marefat, M., Ma, D., Wang, J.M.: Principle Hessian direction-based parameter reduction for interconnect networks with process variation. IEEE Transactions on VLSI Systems 18(9), 1337–1347 (2010)
Nemirovski, A., Shapiro, A.: Convex approximations of chance constrained programs. SIAM Journal on Optimization 17(4), 969–996 (2006)
Palaniappan, S.K., Gyori, B.M., Liu, B., Hsu, D., Thiagarajan, P.S.: Statistical model checking based calibration and analysis of bio-pathway models. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 120–134. Springer, Heidelberg (2013)
Sankaranarayanan, S., Miller, C., Raghunathan, R., Ravanbakhsh, H., Fainekos, G.: A model-based approach to synthesizing insulin infusion pump usage parameters for diabetic patients. In: 2012 50th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pp. 1610–1617 (2012)
Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004)
Singhee, A., Rutenbar, R.A.: Beyond low-order statistical response surfaces: latent variable regression for efficient, highly nonlinear fitting. In: DAC, pp. 256–261 (2007)
Wald, A.: Sequential tests of statistical hypotheses. The Annals of Mathematical Statistics 16(2), 117–186 (1945)
Wang, Y.C., Komuravelli, A., Zuliani, P., Clarke, E.M.: Analog circuit verification by statistical model checking. In: ASP-DAC, pp. 1–6 (2011)
Wie, B., Bernstein, D.S.: A benchmark problem for robust control design. In: American Control Conference, pp. 961–962 (May 1990)
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)
Zhang, Y., Sankaranarayanan, S., Somenzi, F., Chen, X., Ábraham, E.: From statistical model checking to statistical model inference: Characterizing the effect of process variations in analog circuits. In: ICCAD (2013)
Zhang, Y., Sankaranarayanan, S., Somenzi, F., Chen, X., Ábraham, E.: Sparse statistical model inference for analog circuits under process variations. In: ASP-DAC, pp. 449–454 (2014)
Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow/simulink verification. Formal Methods in System Design 43(2), 338–367 (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Zhang, Y., Sankaranarayanan, S., Somenzi, F. (2014). Statistically Sound Verification and Optimization for Complex Systems. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. https://doi.org/10.1007/978-3-319-11936-6_29
Download citation
DOI: https://doi.org/10.1007/978-3-319-11936-6_29
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11935-9
Online ISBN: 978-3-319-11936-6
eBook Packages: Computer ScienceComputer Science (R0)