@ARTICLE{Mancini201612,
author={Mancini, T. and Mari, F. and Massini, A. and Melatti, I. and Tronci, E.},
title={Anytime system level verification via parallel random exhaustive hardware in the loop simulation},
journal={Microprocessors and Microsystems},
year={2016},
volume={41},
pages={12-28},
doi={10.1016/j.micpro.2015.10.010},
note={cited By 0},
url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84954475986&partnerID=40&md5=aaa59999ee06a15ae71fdc764dee32c1},
affiliation={Computer Science Department, Sapienza University of Rome, Italy},
abstract={System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability. © 2015 Elsevier B.V. All rights reserved.},
author_keywords={Hardware in the loop simulation;  Model checking driven simulation;  Model Checking of Hybrid Systems},
keywords={Embedded systems;  Formal verification;  Hardware;  Hybrid systems;  Probability;  Reconfigurable hardware;  Synthetic apertures;  Traction (friction);  Verification, Actual system;  Anytime systems;  Cyber physical systems (CPSs);  Hardware in-the-loop simulation;  Inverted pendulum;  Model checker;  Operational scenario;  Verification process, Model checking},
references={Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proceeding of DSD 2014, pp. 236-245. , IEEE; Baier, C., Katoen, J., (2008) Principles of Model Checking, , MIT Press; Yang, Z., Hu, K., Ma, D., Bodeveix, J.-P., Pi, L., Talpin, J.-P., From {AADL} to timed abstract state machines: A verified model transformation (2014) J. Syst. Softw., 93, pp. 42-68. , http://dx.doi.org/10.1016/j.jss.2014.02.058; Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M., From aadl model to lnt specification (2015) Reliable Software Technologies Ada-Europe 2015, 9111, pp. 146-161. , J.A. de la Puente, T. Vardanega, Lecture Notes in Computer Science Springer International Publishing; Clarke, E., Henzinger, T., Veith, H., (2016) Handbook of Model Checking, , Springer; Alur, R., Formal verification of hybrid systems (2011) Proceedings of EMSOFT 2011, pp. 273-278. , ACM; Clarke, E.M., Jr., Grumberg, O., Peled, D.A., (1999) Model Checking, , MIT Press Cambridge, MA, USA; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proceedings of CAV 2013, 8044, pp. 296-312. , Lecture Notes in Computer Science Springer; Aloul, F.A., Sierawski, B.D., Sakallah, K.A., Satometer: How much have we searched? (2002) Proceedings of the 39th Annual Design Automation Conference, pp. 737-742. , DAC '02 ACM New York, NY, USA; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proceedings of TACAS 2005, 3440, pp. 271-286. , N. Halbwachs, L.D. Zuck, LNCS Springer; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , Texts in Applied Mathematics Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proceedings of PDP 2014, pp. 734-742. , IEEE; Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M., Exploiting transition locality in automatic verification of finite state concurrent systems (2004) STTT, 6 (4), pp. 320-341; Maler, O., Nickovic, D., Monitoring temporal properties of continuous signals (2004) Proceedings of FORMATS 2004 and FTRTFT 2004, 3253, pp. 152-166. , LNCS; Clarke, E.M., Donz, A., Legay, A., On simulation-based probabilistic model checking of mixed-analog circuits. (2010) Form. Methods Syst. Des., 36 (2), pp. 97-113; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to simulink/stateflow verification (2010) Proceedings of HSCC 2010, pp. 243-252; Kim, Y.J., Kim, M., Hybrid statistical model checking technique for reliable safety critical systems (2012) Proceedings of ISSRE 2012, pp. 51-60; Kim, Y.J., Choi, O., Kim, M., Baik, J., Kim, T., Validating software reliability early through statistical model checking (2013) IEEE Softw., 30 (3), pp. 35-41; Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienmüller, T., Incremental bounded model checking for embedded software (extended version) (2014) CoRR, , CoRR abs/1409.5872 2014, 14095872; http://www.mathworks.com/help/stateflow/examples/modeling-a-fault-tolerant-fuel-control-system.html, MathWorks, Modeling a fault tolerant fuel control system, (accessed 11.10.15)Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., SyLVaaS: System Level Formal Verification as a Service (2015) Proceedings of PDP 2015, pp. 476-483. , IEEE; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proceedings of APSEC 2001, pp. 317-324. , IEEE; Sivaraj, H., Gopalakrishnan, G., Random walk based heuristic algorithms for distributed memory model checking. (2003) Electr. Notes Theor. Comput. Sci., 89 (1), pp. 51-67; Arcuri, A., Iqbal, M., Briand, L., Random testing: Theoretical results and practical implications (2012) IEEE Trans. Softw. Eng., 38 (2), pp. 258-277; Motwani, R., Raghavan, P., (1995) Randomized Algorithms, , Cambridge University Press New York, NY, USA; Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A., Probabilistic temporal logic falsification of cyber-physical systems (2013) ACM Trans. Embed. Comput. Syst., 12 S, pp. 951-9530; Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V., Finite horizon analysis of Markov chains with the Murphi verifier. (2006) STTT, 8 (4-5), pp. 397-409; Jansen, D., Katoen, J., Oldenkamp, M., Stoelinga, M., Zapreev, I., How fast and fat is your probabilistic model checker? An experimental performance comparison (2008) Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007, 4899, pp. 69-85. , K. Yohav, Lecture Notes in Computer Science Springer Verlag London; Younes, H.L.S., Simmons, R.G., Probabilistic verification of discrete event systems using acceptance sampling (2002) CAV Lecture Notes in Computer Science Springer, 2404, pp. 223-235. , E. Brinksma, K.G. Larsen; Younes, H.L.S., Ymer: A statistical model checker (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 429-433. , K. Etessami, S.K. Rajamani; Younes, H.L.S., Probabilistic verification for "black-box" systems (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 253-265. , K. Etessami, S.K. Rajamani; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 266-280. , K. Etessami, S.K. Rajamani; Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D., Numerical vs. Statistical probabilistic model checking (2006) STTT, 8 (3), pp. 216-228; David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z., Time for statistical model checking of real-time systems (2011) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), 6806, pp. 349-355. , G. Gopalakrishnan, S. Qadeer, LNCS Springer-Verlag Berlin, Heidelberg; Tripakis, S., Sofronis, C., Caspi, P., Curic, A., Translating discrete-time simulink to lustre (2005) ACM Trans. Emb. Comp. Syst., 4 (4), pp. 779-818; Meenakshi, B., Bhatnagar, A., Roy, S., Tool for translating simulink models into input language of a model checker (2006) Proceedings of ICFEM 2006, pp. 606-620; Whalen, M., Cofer, D., Miller, S., Krogh, B., Storm, W., Integration of formal analysis into a model-based software development process (2007) Proceedings of FMICS 2007, pp. 68-84},
correspondence_address1={Mancini, T.; Computer Science Department, Sapienza University of RomeItaly; email: tmancini@di.uniroma1.it},
publisher={Elsevier},
issn={01419331},
coden={MIMID},
language={English},
abbrev_source_title={Microprocessors Microsyst},
document_type={Article},
source={Scopus},
}

{"_id":"BHWyhGiRfodWm6z8E","bibbaseid":"mancini-mari-massini-melatti-tronci-anytimesystemlevelverificationviaparallelrandomexhaustivehardwareintheloopsimulation-2016","downloads":0,"creationDate":"2016-10-14T09:18:19.797Z","title":"Anytime system level verification via parallel random exhaustive hardware in the loop simulation","author_short":["Mancini, T.","Mari, F.","Massini, A.","Melatti, I.","Tronci, E."],"year":2016,"bibtype":"article","biburl":"http://mari.di.uniroma1.it/fmPubs.bib","bibdata":{"bibtype":"article","type":"article","author":[{"propositions":[],"lastnames":["Mancini"],"firstnames":["T."],"suffixes":[]},{"propositions":[],"lastnames":["Mari"],"firstnames":["F."],"suffixes":[]},{"propositions":[],"lastnames":["Massini"],"firstnames":["A."],"suffixes":[]},{"propositions":[],"lastnames":["Melatti"],"firstnames":["I."],"suffixes":[]},{"propositions":[],"lastnames":["Tronci"],"firstnames":["E."],"suffixes":[]}],"title":"Anytime system level verification via parallel random exhaustive hardware in the loop simulation","journal":"Microprocessors and Microsystems","year":"2016","volume":"41","pages":"12-28","doi":"10.1016/j.micpro.2015.10.010","note":"cited By 0","url":"https://www.scopus.com/inward/record.uri?eid=2-s2.0-84954475986&partnerID=40&md5=aaa59999ee06a15ae71fdc764dee32c1","affiliation":"Computer Science Department, Sapienza University of Rome, Italy","abstract":"System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability. © 2015 Elsevier B.V. All rights reserved.","author_keywords":"Hardware in the loop simulation; Model checking driven simulation; Model Checking of Hybrid Systems","keywords":"Embedded systems; Formal verification; Hardware; Hybrid systems; Probability; Reconfigurable hardware; Synthetic apertures; Traction (friction); Verification, Actual system; Anytime systems; Cyber physical systems (CPSs); Hardware in-the-loop simulation; Inverted pendulum; Model checker; Operational scenario; Verification process, Model checking","references":"Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proceeding of DSD 2014, pp. 236-245. , IEEE; Baier, C., Katoen, J., (2008) Principles of Model Checking, , MIT Press; Yang, Z., Hu, K., Ma, D., Bodeveix, J.-P., Pi, L., Talpin, J.-P., From AADL to timed abstract state machines: A verified model transformation (2014) J. Syst. Softw., 93, pp. 42-68. , http://dx.doi.org/10.1016/j.jss.2014.02.058; Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M., From aadl model to lnt specification (2015) Reliable Software Technologies Ada-Europe 2015, 9111, pp. 146-161. , J.A. de la Puente, T. Vardanega, Lecture Notes in Computer Science Springer International Publishing; Clarke, E., Henzinger, T., Veith, H., (2016) Handbook of Model Checking, , Springer; Alur, R., Formal verification of hybrid systems (2011) Proceedings of EMSOFT 2011, pp. 273-278. , ACM; Clarke, E.M., Jr., Grumberg, O., Peled, D.A., (1999) Model Checking, , MIT Press Cambridge, MA, USA; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proceedings of CAV 2013, 8044, pp. 296-312. , Lecture Notes in Computer Science Springer; Aloul, F.A., Sierawski, B.D., Sakallah, K.A., Satometer: How much have we searched? (2002) Proceedings of the 39th Annual Design Automation Conference, pp. 737-742. , DAC '02 ACM New York, NY, USA; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proceedings of TACAS 2005, 3440, pp. 271-286. , N. Halbwachs, L.D. Zuck, LNCS Springer; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , Texts in Applied Mathematics Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proceedings of PDP 2014, pp. 734-742. , IEEE; Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M., Exploiting transition locality in automatic verification of finite state concurrent systems (2004) STTT, 6 (4), pp. 320-341; Maler, O., Nickovic, D., Monitoring temporal properties of continuous signals (2004) Proceedings of FORMATS 2004 and FTRTFT 2004, 3253, pp. 152-166. , LNCS; Clarke, E.M., Donz, A., Legay, A., On simulation-based probabilistic model checking of mixed-analog circuits. (2010) Form. Methods Syst. Des., 36 (2), pp. 97-113; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to simulink/stateflow verification (2010) Proceedings of HSCC 2010, pp. 243-252; Kim, Y.J., Kim, M., Hybrid statistical model checking technique for reliable safety critical systems (2012) Proceedings of ISSRE 2012, pp. 51-60; Kim, Y.J., Choi, O., Kim, M., Baik, J., Kim, T., Validating software reliability early through statistical model checking (2013) IEEE Softw., 30 (3), pp. 35-41; Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienmüller, T., Incremental bounded model checking for embedded software (extended version) (2014) CoRR, , CoRR abs/1409.5872 2014, 14095872; http://www.mathworks.com/help/stateflow/examples/modeling-a-fault-tolerant-fuel-control-system.html, MathWorks, Modeling a fault tolerant fuel control system, (accessed 11.10.15)Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., SyLVaaS: System Level Formal Verification as a Service (2015) Proceedings of PDP 2015, pp. 476-483. , IEEE; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proceedings of APSEC 2001, pp. 317-324. , IEEE; Sivaraj, H., Gopalakrishnan, G., Random walk based heuristic algorithms for distributed memory model checking. (2003) Electr. Notes Theor. Comput. Sci., 89 (1), pp. 51-67; Arcuri, A., Iqbal, M., Briand, L., Random testing: Theoretical results and practical implications (2012) IEEE Trans. Softw. Eng., 38 (2), pp. 258-277; Motwani, R., Raghavan, P., (1995) Randomized Algorithms, , Cambridge University Press New York, NY, USA; Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A., Probabilistic temporal logic falsification of cyber-physical systems (2013) ACM Trans. Embed. Comput. Syst., 12 S, pp. 951-9530; Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V., Finite horizon analysis of Markov chains with the Murphi verifier. (2006) STTT, 8 (4-5), pp. 397-409; Jansen, D., Katoen, J., Oldenkamp, M., Stoelinga, M., Zapreev, I., How fast and fat is your probabilistic model checker? An experimental performance comparison (2008) Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007, 4899, pp. 69-85. , K. Yohav, Lecture Notes in Computer Science Springer Verlag London; Younes, H.L.S., Simmons, R.G., Probabilistic verification of discrete event systems using acceptance sampling (2002) CAV Lecture Notes in Computer Science Springer, 2404, pp. 223-235. , E. Brinksma, K.G. Larsen; Younes, H.L.S., Ymer: A statistical model checker (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 429-433. , K. Etessami, S.K. Rajamani; Younes, H.L.S., Probabilistic verification for \"black-box\" systems (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 253-265. , K. Etessami, S.K. Rajamani; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 266-280. , K. Etessami, S.K. Rajamani; Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D., Numerical vs. Statistical probabilistic model checking (2006) STTT, 8 (3), pp. 216-228; David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z., Time for statistical model checking of real-time systems (2011) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), 6806, pp. 349-355. , G. Gopalakrishnan, S. Qadeer, LNCS Springer-Verlag Berlin, Heidelberg; Tripakis, S., Sofronis, C., Caspi, P., Curic, A., Translating discrete-time simulink to lustre (2005) ACM Trans. Emb. Comp. Syst., 4 (4), pp. 779-818; Meenakshi, B., Bhatnagar, A., Roy, S., Tool for translating simulink models into input language of a model checker (2006) Proceedings of ICFEM 2006, pp. 606-620; Whalen, M., Cofer, D., Miller, S., Krogh, B., Storm, W., Integration of formal analysis into a model-based software development process (2007) Proceedings of FMICS 2007, pp. 68-84","correspondence_address1":"Mancini, T.; Computer Science Department, Sapienza University of RomeItaly; email: tmancini@di.uniroma1.it","publisher":"Elsevier","issn":"01419331","coden":"MIMID","language":"English","abbrev_source_title":"Microprocessors Microsyst","document_type":"Article","source":"Scopus","bibtex":"@ARTICLE{Mancini201612,\nauthor={Mancini, T. and Mari, F. and Massini, A. and Melatti, I. and Tronci, E.},\ntitle={Anytime system level verification via parallel random exhaustive hardware in the loop simulation},\njournal={Microprocessors and Microsystems},\nyear={2016},\nvolume={41},\npages={12-28},\ndoi={10.1016/j.micpro.2015.10.010},\nnote={cited By 0},\nurl={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84954475986&partnerID=40&md5=aaa59999ee06a15ae71fdc764dee32c1},\naffiliation={Computer Science Department, Sapienza University of Rome, Italy},\nabstract={System level verification of cyber-physical systems has the goal of verifying that the whole (i.e., software + hardware) system meets the given specifications. Model checkers for hybrid systems cannot handle system level verification of actual systems. Thus, Hardware In the Loop Simulation (HILS) is currently the main workhorse for system level verification. By using model checking driven exhaustive HILS, System Level Formal Verification (SLFV) can be effectively carried out for actual systems. We present a parallel random exhaustive HILS based model checker for hybrid systems that, by simulating all operational scenarios exactly once in a uniform random order, is able to provide, at any time during the verification process, an upper bound to the probability that the System Under Verification exhibits an error in a yet-to-be-simulated scenario (Omission Probability). We show effectiveness of the proposed approach by presenting experimental results on SLFV of the Inverted Pendulum on a Cart and the Fuel Control System examples in the Simulink distribution. To the best of our knowledge, no previously published model checker can exhaustively verify hybrid systems of such a size and provide at any time an upper bound to the Omission Probability. © 2015 Elsevier B.V. All rights reserved.},\nauthor_keywords={Hardware in the loop simulation; Model checking driven simulation; Model Checking of Hybrid Systems},\nkeywords={Embedded systems; Formal verification; Hardware; Hybrid systems; Probability; Reconfigurable hardware; Synthetic apertures; Traction (friction); Verification, Actual system; Anytime systems; Cyber physical systems (CPSs); Hardware in-the-loop simulation; Inverted pendulum; Model checker; Operational scenario; Verification process, Model checking},\nreferences={Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., Anytime system level verification via random exhaustive hardware in the loop simulation (2014) Proceeding of DSD 2014, pp. 236-245. , IEEE; Baier, C., Katoen, J., (2008) Principles of Model Checking, , MIT Press; Yang, Z., Hu, K., Ma, D., Bodeveix, J.-P., Pi, L., Talpin, J.-P., From {AADL} to timed abstract state machines: A verified model transformation (2014) J. Syst. Softw., 93, pp. 42-68. , http://dx.doi.org/10.1016/j.jss.2014.02.058; Mkaouar, H., Zalila, B., Hugues, J., Jmaiel, M., From aadl model to lnt specification (2015) Reliable Software Technologies Ada-Europe 2015, 9111, pp. 146-161. , J.A. de la Puente, T. Vardanega, Lecture Notes in Computer Science Springer International Publishing; Clarke, E., Henzinger, T., Veith, H., (2016) Handbook of Model Checking, , Springer; Alur, R., Formal verification of hybrid systems (2011) Proceedings of EMSOFT 2011, pp. 273-278. , ACM; Clarke, E.M., Jr., Grumberg, O., Peled, D.A., (1999) Model Checking, , MIT Press Cambridge, MA, USA; Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proceedings of CAV 2013, 8044, pp. 296-312. , Lecture Notes in Computer Science Springer; Aloul, F.A., Sierawski, B.D., Sakallah, K.A., Satometer: How much have we searched? (2002) Proceedings of the 39th Annual Design Automation Conference, pp. 737-742. , DAC '02 ACM New York, NY, USA; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proceedings of TACAS 2005, 3440, pp. 271-286. , N. Halbwachs, L.D. Zuck, LNCS Springer; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , Texts in Applied Mathematics Springer; Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., System level formal verification via distributed multi-core hardware in the loop simulation (2014) Proceedings of PDP 2014, pp. 734-742. , IEEE; Della Penna, G., Intrigila, B., Melatti, I., Tronci, E., Venturini Zilli, M., Exploiting transition locality in automatic verification of finite state concurrent systems (2004) STTT, 6 (4), pp. 320-341; Maler, O., Nickovic, D., Monitoring temporal properties of continuous signals (2004) Proceedings of FORMATS 2004 and FTRTFT 2004, 3253, pp. 152-166. , LNCS; Clarke, E.M., Donz, A., Legay, A., On simulation-based probabilistic model checking of mixed-analog circuits. (2010) Form. Methods Syst. Des., 36 (2), pp. 97-113; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to simulink/stateflow verification (2010) Proceedings of HSCC 2010, pp. 243-252; Kim, Y.J., Kim, M., Hybrid statistical model checking technique for reliable safety critical systems (2012) Proceedings of ISSRE 2012, pp. 51-60; Kim, Y.J., Choi, O., Kim, M., Baik, J., Kim, T., Validating software reliability early through statistical model checking (2013) IEEE Softw., 30 (3), pp. 35-41; Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienmüller, T., Incremental bounded model checking for embedded software (extended version) (2014) CoRR, , CoRR abs/1409.5872 2014, 14095872; http://www.mathworks.com/help/stateflow/examples/modeling-a-fault-tolerant-fuel-control-system.html, MathWorks, Modeling a fault tolerant fuel control system, (accessed 11.10.15)Mancini, T., Mari, F., Massini, A., Melatti, I., Tronci, E., SyLVaaS: System Level Formal Verification as a Service (2015) Proceedings of PDP 2015, pp. 476-483. , IEEE; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proceedings of APSEC 2001, pp. 317-324. , IEEE; Sivaraj, H., Gopalakrishnan, G., Random walk based heuristic algorithms for distributed memory model checking. (2003) Electr. Notes Theor. Comput. Sci., 89 (1), pp. 51-67; Arcuri, A., Iqbal, M., Briand, L., Random testing: Theoretical results and practical implications (2012) IEEE Trans. Softw. Eng., 38 (2), pp. 258-277; Motwani, R., Raghavan, P., (1995) Randomized Algorithms, , Cambridge University Press New York, NY, USA; Abbas, H., Fainekos, G., Sankaranarayanan, S., Ivančić, F., Gupta, A., Probabilistic temporal logic falsification of cyber-physical systems (2013) ACM Trans. Embed. Comput. Syst., 12 S, pp. 951-9530; Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V., Finite horizon analysis of Markov chains with the Murphi verifier. (2006) STTT, 8 (4-5), pp. 397-409; Jansen, D., Katoen, J., Oldenkamp, M., Stoelinga, M., Zapreev, I., How fast and fat is your probabilistic model checker? An experimental performance comparison (2008) Hardware and Software: Verification and Testing, Proceedings of the Third International Haifa Verification Conference, HVC 2007, 4899, pp. 69-85. , K. Yohav, Lecture Notes in Computer Science Springer Verlag London; Younes, H.L.S., Simmons, R.G., Probabilistic verification of discrete event systems using acceptance sampling (2002) CAV Lecture Notes in Computer Science Springer, 2404, pp. 223-235. , E. Brinksma, K.G. Larsen; Younes, H.L.S., Ymer: A statistical model checker (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 429-433. , K. Etessami, S.K. Rajamani; Younes, H.L.S., Probabilistic verification for \"black-box\" systems (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 253-265. , K. Etessami, S.K. Rajamani; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) CAV Lecture Notes in Computer Science Springer, 3576, pp. 266-280. , K. Etessami, S.K. Rajamani; Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D., Numerical vs. Statistical probabilistic model checking (2006) STTT, 8 (3), pp. 216-228; David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z., Time for statistical model checking of real-time systems (2011) Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), 6806, pp. 349-355. , G. Gopalakrishnan, S. Qadeer, LNCS Springer-Verlag Berlin, Heidelberg; Tripakis, S., Sofronis, C., Caspi, P., Curic, A., Translating discrete-time simulink to lustre (2005) ACM Trans. Emb. Comp. Syst., 4 (4), pp. 779-818; Meenakshi, B., Bhatnagar, A., Roy, S., Tool for translating simulink models into input language of a model checker (2006) Proceedings of ICFEM 2006, pp. 606-620; Whalen, M., Cofer, D., Miller, S., Krogh, B., Storm, W., Integration of formal analysis into a model-based software development process (2007) Proceedings of FMICS 2007, pp. 68-84},\ncorrespondence_address1={Mancini, T.; Computer Science Department, Sapienza University of RomeItaly; email: tmancini@di.uniroma1.it},\npublisher={Elsevier},\nissn={01419331},\ncoden={MIMID},\nlanguage={English},\nabbrev_source_title={Microprocessors Microsyst},\ndocument_type={Article},\nsource={Scopus},\n}\n\n","author_short":["Mancini, T.","Mari, F.","Massini, A.","Melatti, I.","Tronci, E."],"key":"Mancini201612","id":"Mancini201612","bibbaseid":"mancini-mari-massini-melatti-tronci-anytimesystemlevelverificationviaparallelrandomexhaustivehardwareintheloopsimulation-2016","role":"author","urls":{"Paper":"https://www.scopus.com/inward/record.uri?eid=2-s2.0-84954475986&partnerID=40&md5=aaa59999ee06a15ae71fdc764dee32c1"},"keyword":["Embedded systems; Formal verification; Hardware; Hybrid systems; Probability; Reconfigurable hardware; Synthetic apertures; Traction (friction); Verification","Actual system; Anytime systems; Cyber physical systems (CPSs); Hardware in-the-loop simulation; Inverted pendulum; Model checker; Operational scenario; Verification process","Model checking"],"downloads":0},"search_terms":["anytime","system","level","verification","via","parallel","random","exhaustive","hardware","loop","simulation","mancini","mari","massini","melatti","tronci"],"keywords":["embedded systems; formal verification; hardware; hybrid systems; probability; reconfigurable hardware; synthetic apertures; traction (friction); verification","actual system; anytime systems; cyber physical systems (cpss); hardware in-the-loop simulation; inverted pendulum; model checker; operational scenario; verification process","model checking"],"authorIDs":[],"dataSources":["L3NrffcQCrJ5r6svQ"]}