×

Probabilistic verification of a biodiesel production system using statistical model checking. (English) Zbl 1299.90129

Summary: Biochemical system designers are increasingly using formal modelling, simulation, and verification methods to improve the understanding of complex systems. Probabilistic models can incorporate realistic stochastic dynamics, but creating and analysing probabilistic models in a formal way is challenging. In this work, we present a stochastic model of biodiesel production that incorporates an inexpensive test of fuel quality, and we validate the model using statistical model checking, which can be used to evaluate simple or complex temporal properties efficiently. We also describe probabilistic simulation and analysis techniques for stochastic hybrid system (SHS) models to demonstrate the properties of our model. We introduce a variety of properties for various configurations of the reactor as well as results of testing our model against the properties.

MSC:

90B30 Production models
93E03 Stochastic systems in control theory (general)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1016/j.biortech.2005.11.022 · doi:10.1016/j.biortech.2005.11.022
[2] Haas M., A process model to estimate biodiesel production costs. Bioresour. Technol. 97 (671) pp 671– (2006)
[3] DOI: 10.1021/ef0503764 · doi:10.1021/ef0503764
[4] DOI: 10.1007/s11746-997-0254-2 · doi:10.1007/s11746-997-0254-2
[5] Jaya N., IJEST 3 (4) pp 3463– (2011)
[6] West A., Bioresour. Technol. 99 (14) pp 6587– (2007)
[7] DOI: 10.1016/S0960-8524(03)00040-3 · doi:10.1016/S0960-8524(03)00040-3
[8] DOI: 10.1021/ie101403f · doi:10.1021/ie101403f
[9] Riley D., Eur. J. Control: Special Issue on Stochastic Hybrid Systems. 16 (6) pp 609– (2010) · Zbl 1214.90044 · doi:10.3166/ejc.16.609-623
[10] DOI: 10.1287/opre.47.4.585 · Zbl 0985.65006 · doi:10.1287/opre.47.4.585
[11] DOI: 10.1016/j.tcs.2010.02.010 · Zbl 1209.68310 · doi:10.1016/j.tcs.2010.02.010
[12] Ballarini P., PDMC 14 pp 47– (2009)
[13] DOI: 10.1007/BFb0025774 · doi:10.1007/BFb0025774
[14] S.K. Jha, E.M. Clarke, C.J. Langmead, A. Legay, A. Platzer, and P. Zuliani,A Bayesian Approach to Model Checking Biological Systems, Proceedings of the 7th International Conference on Computational Methods in Systems Biology, CMSB ’09, pp. 218–234, Berlin, Heidelberg, 2009. Springer-Verlag.
[15] Legay A., ArXiv e-prints (2010)
[16] DOI: 10.1016/j.ic.2006.05.002 · Zbl 1110.68077 · doi:10.1016/j.ic.2006.05.002
[17] Abate A., Hybrid Syst. Comput. Control LNCS 4416 pp 4– (2007) · Zbl 1221.93030 · doi:10.1007/978-3-540-71493-4_4
[18] Bernadskiy M., Formats LNCS 3253 pp 309– (2004)
[19] Blom H., IEEE Conference on Decision and Control pp 3182– (2007)
[20] Bujorianu M., IEEE Conference on Decision and Control (2004)
[21] DOI: 10.1007/978-3-540-24743-2_26 · doi:10.1007/978-3-540-24743-2_26
[22] Riley D., Hybrid Syst. Comput. Control LNCS 4416 pp 758– (2007) · Zbl 05527825 · doi:10.1007/978-3-540-71493-4_78
[23] DOI: 10.1109/WSC.2008.4736143 · doi:10.1109/WSC.2008.4736143
[24] Jazwinski A., Academic Press, Waltham, MA (1970)
[25] DOI: 10.1109/TSMCA.2007.914777 · doi:10.1109/TSMCA.2007.914777
[26] DOI: 10.1049/iet-syb.2008.0101 · doi:10.1049/iet-syb.2008.0101
[27] Kloeden P., Numerical Solution of Stochastic Differential Equations (1999)
[28] DOI: 10.1051/ps:2001112 · Zbl 0998.60081 · doi:10.1051/ps:2001112
[29] DOI: 10.1016/j.simpat.2010.05.021 · Zbl 06019873 · doi:10.1016/j.simpat.2010.05.021
[30] Younes H., CAV, LCNS 2404 pp 223– (2002)
[31] Riley D., Multilevel splitting for reachability analysis of stochastic hybrid systems, Summer Simulation Multiconference, Ottawa, ON, July (2010)
[32] Troyer M., ISCOPE LNCS 1505 pp 191– (1998)
[33] DOI: 10.1016/j.energy.2006.06.019 · doi:10.1016/j.energy.2006.06.019
[34] Hespanha J., Int. J. Robust Cont., Special Issue on Control at Small Scales 15 pp 669– (2005)
[35] DOI: 10.1016/0021-9991(76)90041-3 · doi:10.1016/0021-9991(76)90041-3
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.