@CONFERENCE{Mancini2014734,
author={Mancini, T. and Mari, F. and Massini, A. and Melatti, I. and Tronci, E.},
title={System level formal verification via distributed multi-core hardware in the loop simulation},
journal={Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014},
year={2014},
pages={734-742},
doi={10.1109/PDP.2014.32},
art_number={6787353},
note={cited By 8; Conference of 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014 ; Conference Date: 12 February 2014 Through 14 February 2014;  Conference Code:104780},
url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84899430374&partnerID=40&md5=06b4fcf5b92af5440acc55454201a97d},
affiliation={Computer Science Department, Sapienza University of Rome, Via Salaria 113, I-00198 Roma, Italy},
abstract={The goal of System Level Formal Verification (SLFV) is to show system correctness notwithstanding uncontrollable events (such as: faults, variation in system parameters, external inputs, etc). Hardware In the Loop Simulation (HILS) based SLFV attains such a goal by considering exhaustively all relevant simulation scenarios. We present a distributed multi-core algorithm for HILS-based SLFV. Our experimental results on the Fuel Control System example in the Simulink distribution show that by using 64 machines with an 8 core processor each we can complete the SLFV activity in about 27 hours whereas a sequential approach would require more than 200 days. To the best of our knowledge this is the first time that a distributed multi-core algorithm for HILS-based SLFV is presented. © 2014 IEEE.},
author_keywords={Distributed Multi-Core Hardware in the Loops Simulation;  Hybrid Systems;  Model Checking;  System Level Formal Verification},
keywords={Algorithms;  Hybrid systems;  Model checking, Core processors;  External input;  Formal verifications;  Hard-ware-in-the-loop;  Hardware-in-the-loop simulation;  Multi-core algorithm;  Sequential approach;  System levels, Traction (friction)},
references={Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proc. CAV 2013, Ser. LNCS, 8044, pp. 296-312. , Springer; Alur, R., Formal verification of hybrid systems (2011) Proc. EMSOFT 2011, pp. 273-278. , ACM; Cavaliere, F., Mari, F., Melatti, I., Minei, G., Salvo, I., Tronci, E., Verzino, G., Yushtein, Y., Model checking satellite operational procedures (2011) Proc. DASIA 2011; 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; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to simulink/stateflow verification (2010) Proc. HSCC 2010, pp. 243-252; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) Proc. CAV 2005, Ser. LNCS, 3576, pp. 266-280. , Springer; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proc. APSEC 2001, , IEEE; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proc. TACAS 2005, Ser. LNCS, 3440. , Springer; 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) Proc. 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) Proc. FMICS 2007; Yang, C., Dill, D., Validation with guided search of the state space (1998) Proc. DAC1 1998, pp. 599-604. , ACM; Ho, P., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J., Smart simulation using collaborative formal and simulation engines (2000) Proc. ICCAD 2000, pp. 120-126. , IEEE; Nanshi, K., Somenzi, F., Guiding simulation with increasingly refined abstract traces (2006) Proc. DAC 2006, pp. 737-742. , ACM; De Paula, F., Hu, A., An effective guidance strategy for abstraction-guided simulation (2007) Proc. DAC 2007, pp. 63-68. , ACM; Stern, U., Dill, D., Parallelizing the Murphi verifier (2001) Form. Methods Syst. Des., 18 (2), pp. 117-129; Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P., Divine: A tool for distributed verification (2006) Proc. CAV 2006, pp. 278-281. , Springer; Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R., Gopalakrishnan, G., Parallel and distributed model checking in eddy (2009) Int. J. Softw. Tools Technol. Transf., 11 (1), pp. 13-25; Bingham, B., Bingham, J., De Paula, F., Erickson, J., Singh, G., Reitblatt, M., Industrial strength distributed explicit state model checking (2010) Proc. PDMC-HIBI 2010, pp. 28-36. , IEEE; Holzmann, G., Parallelizing the SPIN model checker (2012) Proc. SPIN 2012, pp. 155-171. , Springer; Laarman, A., Pol De J.Van, Weber, M., Boosting multi-core reachability performance with shared hash tables (2010) Proc. FMCAD 2010, pp. 247-255. , IEEE; Wijs, A., Towards informed swarm verification (2011) Proc. NFM 2011, Ser. LNCS, 6617. , Springer; Staats, M., Pasareanu, C.S., Parallel symbolic execution for structural test generation (2010) Proc. ISSTA 2010, pp. 183-194. , ACM; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , Springer; Maler, O., Nickovic, D., Monitoring temporal properties of continuous signals (2004) Proc. FORMATS 2004 and FTRTFT 2004, Ser. LNCS, 3253, pp. 152-166},
sponsors={E4 Computer Engineering; IBM Corporation; NVidia Corporation; Sistemi HS (HP ServiceOne expert)},
publisher={IEEE Computer Society},
address={Turin},
language={English},
abbrev_source_title={Proc. - Euromicro Int. Conf. Parallel, Distrib., Netw.-Based Process., PDP},
document_type={Conference Paper},
source={Scopus},
}

{"_id":"QrSHdpQBfCFJpPJtb","bibbaseid":"mancini-mari-massini-melatti-tronci-systemlevelformalverificationviadistributedmulticorehardwareintheloopsimulation-2014","downloads":0,"creationDate":"2016-10-14T09:18:19.768Z","title":"System level formal verification via distributed multi-core hardware in the loop simulation","author_short":["Mancini, T.","Mari, F.","Massini, A.","Melatti, I.","Tronci, E."],"year":2014,"bibtype":"conference","biburl":"http://mari.di.uniroma1.it/fmPubs.bib","bibdata":{"bibtype":"conference","type":"conference","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":"System level formal verification via distributed multi-core hardware in the loop simulation","journal":"Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014","year":"2014","pages":"734-742","doi":"10.1109/PDP.2014.32","art_number":"6787353","note":"cited By 8; Conference of 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014 ; Conference Date: 12 February 2014 Through 14 February 2014; Conference Code:104780","url":"https://www.scopus.com/inward/record.uri?eid=2-s2.0-84899430374&partnerID=40&md5=06b4fcf5b92af5440acc55454201a97d","affiliation":"Computer Science Department, Sapienza University of Rome, Via Salaria 113, I-00198 Roma, Italy","abstract":"The goal of System Level Formal Verification (SLFV) is to show system correctness notwithstanding uncontrollable events (such as: faults, variation in system parameters, external inputs, etc). Hardware In the Loop Simulation (HILS) based SLFV attains such a goal by considering exhaustively all relevant simulation scenarios. We present a distributed multi-core algorithm for HILS-based SLFV. Our experimental results on the Fuel Control System example in the Simulink distribution show that by using 64 machines with an 8 core processor each we can complete the SLFV activity in about 27 hours whereas a sequential approach would require more than 200 days. To the best of our knowledge this is the first time that a distributed multi-core algorithm for HILS-based SLFV is presented. © 2014 IEEE.","author_keywords":"Distributed Multi-Core Hardware in the Loops Simulation; Hybrid Systems; Model Checking; System Level Formal Verification","keywords":"Algorithms; Hybrid systems; Model checking, Core processors; External input; Formal verifications; Hard-ware-in-the-loop; Hardware-in-the-loop simulation; Multi-core algorithm; Sequential approach; System levels, Traction (friction)","references":"Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proc. CAV 2013, Ser. LNCS, 8044, pp. 296-312. , Springer; Alur, R., Formal verification of hybrid systems (2011) Proc. EMSOFT 2011, pp. 273-278. , ACM; Cavaliere, F., Mari, F., Melatti, I., Minei, G., Salvo, I., Tronci, E., Verzino, G., Yushtein, Y., Model checking satellite operational procedures (2011) Proc. DASIA 2011; 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; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to simulink/stateflow verification (2010) Proc. HSCC 2010, pp. 243-252; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) Proc. CAV 2005, Ser. LNCS, 3576, pp. 266-280. , Springer; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proc. APSEC 2001, , IEEE; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proc. TACAS 2005, Ser. LNCS, 3440. , Springer; 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) Proc. 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) Proc. FMICS 2007; Yang, C., Dill, D., Validation with guided search of the state space (1998) Proc. DAC1 1998, pp. 599-604. , ACM; Ho, P., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J., Smart simulation using collaborative formal and simulation engines (2000) Proc. ICCAD 2000, pp. 120-126. , IEEE; Nanshi, K., Somenzi, F., Guiding simulation with increasingly refined abstract traces (2006) Proc. DAC 2006, pp. 737-742. , ACM; De Paula, F., Hu, A., An effective guidance strategy for abstraction-guided simulation (2007) Proc. DAC 2007, pp. 63-68. , ACM; Stern, U., Dill, D., Parallelizing the Murphi verifier (2001) Form. Methods Syst. Des., 18 (2), pp. 117-129; Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P., Divine: A tool for distributed verification (2006) Proc. CAV 2006, pp. 278-281. , Springer; Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R., Gopalakrishnan, G., Parallel and distributed model checking in eddy (2009) Int. J. Softw. Tools Technol. Transf., 11 (1), pp. 13-25; Bingham, B., Bingham, J., De Paula, F., Erickson, J., Singh, G., Reitblatt, M., Industrial strength distributed explicit state model checking (2010) Proc. PDMC-HIBI 2010, pp. 28-36. , IEEE; Holzmann, G., Parallelizing the SPIN model checker (2012) Proc. SPIN 2012, pp. 155-171. , Springer; Laarman, A., Pol De J.Van, Weber, M., Boosting multi-core reachability performance with shared hash tables (2010) Proc. FMCAD 2010, pp. 247-255. , IEEE; Wijs, A., Towards informed swarm verification (2011) Proc. NFM 2011, Ser. LNCS, 6617. , Springer; Staats, M., Pasareanu, C.S., Parallel symbolic execution for structural test generation (2010) Proc. ISSTA 2010, pp. 183-194. , ACM; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , Springer; Maler, O., Nickovic, D., Monitoring temporal properties of continuous signals (2004) Proc. FORMATS 2004 and FTRTFT 2004, Ser. LNCS, 3253, pp. 152-166","sponsors":"E4 Computer Engineering; IBM Corporation; NVidia Corporation; Sistemi HS (HP ServiceOne expert)","publisher":"IEEE Computer Society","address":"Turin","language":"English","abbrev_source_title":"Proc. - Euromicro Int. Conf. Parallel, Distrib., Netw.-Based Process., PDP","document_type":"Conference Paper","source":"Scopus","bibtex":"@CONFERENCE{Mancini2014734,\nauthor={Mancini, T. and Mari, F. and Massini, A. and Melatti, I. and Tronci, E.},\ntitle={System level formal verification via distributed multi-core hardware in the loop simulation},\njournal={Proceedings - 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014},\nyear={2014},\npages={734-742},\ndoi={10.1109/PDP.2014.32},\nart_number={6787353},\nnote={cited By 8; Conference of 2014 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014 ; Conference Date: 12 February 2014 Through 14 February 2014; Conference Code:104780},\nurl={https://www.scopus.com/inward/record.uri?eid=2-s2.0-84899430374&partnerID=40&md5=06b4fcf5b92af5440acc55454201a97d},\naffiliation={Computer Science Department, Sapienza University of Rome, Via Salaria 113, I-00198 Roma, Italy},\nabstract={The goal of System Level Formal Verification (SLFV) is to show system correctness notwithstanding uncontrollable events (such as: faults, variation in system parameters, external inputs, etc). Hardware In the Loop Simulation (HILS) based SLFV attains such a goal by considering exhaustively all relevant simulation scenarios. We present a distributed multi-core algorithm for HILS-based SLFV. Our experimental results on the Fuel Control System example in the Simulink distribution show that by using 64 machines with an 8 core processor each we can complete the SLFV activity in about 27 hours whereas a sequential approach would require more than 200 days. To the best of our knowledge this is the first time that a distributed multi-core algorithm for HILS-based SLFV is presented. © 2014 IEEE.},\nauthor_keywords={Distributed Multi-Core Hardware in the Loops Simulation; Hybrid Systems; Model Checking; System Level Formal Verification},\nkeywords={Algorithms; Hybrid systems; Model checking, Core processors; External input; Formal verifications; Hard-ware-in-the-loop; Hardware-in-the-loop simulation; Multi-core algorithm; Sequential approach; System levels, Traction (friction)},\nreferences={Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E., System level formal verification via model checking driven simulation (2013) Proc. CAV 2013, Ser. LNCS, 8044, pp. 296-312. , Springer; Alur, R., Formal verification of hybrid systems (2011) Proc. EMSOFT 2011, pp. 273-278. , ACM; Cavaliere, F., Mari, F., Melatti, I., Minei, G., Salvo, I., Tronci, E., Verzino, G., Yushtein, Y., Model checking satellite operational procedures (2011) Proc. DASIA 2011; 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; Zuliani, P., Platzer, A., Clarke, E., Bayesian statistical model checking with application to simulink/stateflow verification (2010) Proc. HSCC 2010, pp. 243-252; Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) Proc. CAV 2005, Ser. LNCS, 3576, pp. 266-280. , Springer; Tronci, E., Della Penna, G., Intrigila, B., Venturini Zilli, M., A probabilistic approach to automatic verification of concurrent systems (2001) Proc. APSEC 2001, , IEEE; Grosu, R., Smolka, S., Monte carlo model checking (2005) Proc. TACAS 2005, Ser. LNCS, 3440. , Springer; 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) Proc. 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) Proc. FMICS 2007; Yang, C., Dill, D., Validation with guided search of the state space (1998) Proc. DAC1 1998, pp. 599-604. , ACM; Ho, P., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J., Smart simulation using collaborative formal and simulation engines (2000) Proc. ICCAD 2000, pp. 120-126. , IEEE; Nanshi, K., Somenzi, F., Guiding simulation with increasingly refined abstract traces (2006) Proc. DAC 2006, pp. 737-742. , ACM; De Paula, F., Hu, A., An effective guidance strategy for abstraction-guided simulation (2007) Proc. DAC 2007, pp. 63-68. , ACM; Stern, U., Dill, D., Parallelizing the Murphi verifier (2001) Form. Methods Syst. Des., 18 (2), pp. 117-129; Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P., Divine: A tool for distributed verification (2006) Proc. CAV 2006, pp. 278-281. , Springer; Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R., Gopalakrishnan, G., Parallel and distributed model checking in eddy (2009) Int. J. Softw. Tools Technol. Transf., 11 (1), pp. 13-25; Bingham, B., Bingham, J., De Paula, F., Erickson, J., Singh, G., Reitblatt, M., Industrial strength distributed explicit state model checking (2010) Proc. PDMC-HIBI 2010, pp. 28-36. , IEEE; Holzmann, G., Parallelizing the SPIN model checker (2012) Proc. SPIN 2012, pp. 155-171. , Springer; Laarman, A., Pol De J.Van, Weber, M., Boosting multi-core reachability performance with shared hash tables (2010) Proc. FMCAD 2010, pp. 247-255. , IEEE; Wijs, A., Towards informed swarm verification (2011) Proc. NFM 2011, Ser. LNCS, 6617. , Springer; Staats, M., Pasareanu, C.S., Parallel symbolic execution for structural test generation (2010) Proc. ISSTA 2010, pp. 183-194. , ACM; Sontag, E., (1998) Mathematical Control Theory: Deterministic Finite Dimensional Systems, , Springer; Maler, O., Nickovic, D., Monitoring temporal properties of continuous signals (2004) Proc. FORMATS 2004 and FTRTFT 2004, Ser. LNCS, 3253, pp. 152-166},\nsponsors={E4 Computer Engineering; IBM Corporation; NVidia Corporation; Sistemi HS (HP ServiceOne expert)},\npublisher={IEEE Computer Society},\naddress={Turin},\nlanguage={English},\nabbrev_source_title={Proc. - Euromicro Int. Conf. Parallel, Distrib., Netw.-Based Process., PDP},\ndocument_type={Conference Paper},\nsource={Scopus},\n}\n\n","author_short":["Mancini, T.","Mari, F.","Massini, A.","Melatti, I.","Tronci, E."],"key":"Mancini2014734","id":"Mancini2014734","bibbaseid":"mancini-mari-massini-melatti-tronci-systemlevelformalverificationviadistributedmulticorehardwareintheloopsimulation-2014","role":"author","urls":{"Paper":"https://www.scopus.com/inward/record.uri?eid=2-s2.0-84899430374&partnerID=40&md5=06b4fcf5b92af5440acc55454201a97d"},"keyword":["Algorithms; Hybrid systems; Model checking","Core processors; External input; Formal verifications; Hard-ware-in-the-loop; Hardware-in-the-loop simulation; Multi-core algorithm; Sequential approach; System levels","Traction (friction)"],"downloads":0},"search_terms":["system","level","formal","verification","via","distributed","multi","core","hardware","loop","simulation","mancini","mari","massini","melatti","tronci"],"keywords":["algorithms; hybrid systems; model checking","core processors; external input; formal verifications; hard-ware-in-the-loop; hardware-in-the-loop simulation; multi-core algorithm; sequential approach; system levels","traction (friction)"],"authorIDs":[],"dataSources":["L3NrffcQCrJ5r6svQ"]}