{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T08:46:13Z","timestamp":1725871573328},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319495828"},{"type":"electronic","value":"9783319495835"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-49583-5_51","type":"book-chapter","created":{"date-parts":[[2016,11,24]],"date-time":"2016-11-24T03:11:09Z","timestamp":1479957069000},"page":"658-674","source":"Crossref","is-referenced-by-count":1,"title":["A Distributed Formal Model for the Analysis and Verification of Arbitration Protocols on MPSoCs Architecture"],"prefix":"10.1007","author":[{"given":"Imen","family":"Ben Hafaiedh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maroua","family":"Ben Slimane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riadh","family":"Robbana","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,25]]},"reference":[{"issue":"5","key":"51_CR1","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1109\/12.509909","volume":"45","author":"LK John","year":"1996","unstructured":"John, L.K., Liu, Y.: Performance model for a prioritized multiple-bus multiprocessor system. IEEE Trans. Comput. 45(5), 580\u2013588 (1996)","journal-title":"IEEE Trans. Comput."},{"key":"51_CR2","doi-asserted-by":"crossref","unstructured":"Yang, Q., Raja, R.: Design and analysis of multiple-bus arbiters with different priority schemes. In: Parallel Architectures (Postconference PARBASE-1990), pp. 276\u2013295 (1990)","DOI":"10.1109\/PARBSE.1990.77148"},{"key":"51_CR3","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1109\/12.16493","volume":"38","author":"F El-Guibaly","year":"1989","unstructured":"El-Guibaly, F.: Design and analysis of arbitration protocols. IEEE Trans. Comput. 38, 161\u2013171 (1989)","journal-title":"IEEE Trans. Comput."},{"issue":"9","key":"51_CR4","first-page":"250","volume":"8","author":"N Doifode","year":"2008","unstructured":"Doifode, N., Padole, D., Bajaj, P.R.: Design and performance analysis of efficient bus arbitration schemes for on-chip shared bus multi-processor SoC. Int. J. Comput. Sci. Netw. Secur. (IJCSNS) 8(9), 250\u2013255 (2008)","journal-title":"Int. J. Comput. Sci. Netw. Secur. (IJCSNS)"},{"key":"51_CR5","doi-asserted-by":"crossref","DOI":"10.1002\/0471786411","volume-title":"RTL Hardware Design Using VHDL: Coding for Efficiency, Portability, and Scalability","author":"PP Chu","year":"2006","unstructured":"Chu, P.P.: RTL Hardware Design Using VHDL: Coding for Efficiency, Portability, and Scalability. Wiley-IEEE Press, Hoboken (2006)"},{"key":"51_CR6","unstructured":"Fassino, J.-P., Stefani, J.-B., Lawall, J.L., Muller, G.: Think: a software framework for component-based operating system kernels. In: 16th IEEE Real Time Systems Symposium (2002)"},{"key":"51_CR7","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM. IEEE Computer Society, pp. 3\u201312 (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"51_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-73196-2_1","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2007","author":"S Graf","year":"2007","unstructured":"Graf, S., Quinton, S.: Contracts for BIP: hierarchical interaction models for compositional verification. In: Derrick, J., Vain, J. (eds.) FORTE 2007. LNCS, vol. 4574, pp. 1\u201318. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73196-2_1"},{"issue":"10","key":"51_CR9","doi-asserted-by":"crossref","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors - structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008)","journal-title":"IEEE Trans. Comput."},{"key":"51_CR10","doi-asserted-by":"crossref","unstructured":"Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for performance optimization in BIP. In: Proceedings of SIES 2009, pp. 152\u2013160 (2009)","DOI":"10.1109\/SIES.2009.5196211"},{"key":"51_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-24690-6_5","volume-title":"Software Engineering and Formal Methods","author":"I Ben-Hafaiedh","year":"2011","unstructured":"Ben-Hafaiedh, I., Graf, S., Mazouz, N.: Distributed implementation of systems with multiparty interactions and priorities. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 38\u201357. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24690-6_5"},{"key":"51_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-68855-6_8","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2008","author":"A Basu","year":"2008","unstructured":"Basu, A., Bidinger, P., Bozga, M., Sifakis, J.: Distributed semantics and implementation for systems with interaction and priority. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds.) FORTE 2008. LNCS, vol. 5048, pp. 116\u2013133. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-68855-6_8"},{"issue":"3","key":"51_CR13","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/BF02943137","volume":"11","author":"C-M Chung","year":"1996","unstructured":"Chung, C.-M., Chiang, D.A., Yang, Q.: A comparative analysis of different arbitration protocols for multiprocessors. J. Comput. Sci. Technol. 11(3), 313\u2013325 (1996)","journal-title":"J. Comput. Sci. Technol."},{"key":"51_CR14","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-0-387-35079-0_28","volume-title":"Formal Description Techniques IX: Theory, Application and Tools","author":"G Chehaibar","year":"1996","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the powerscale $${}^{\\text{ tm }}$$ bus arbitration protocol: an industrial experiment with LOTOS. In: Gotzhein, R., Bredereke, J. (eds.) Formal Description Techniques IX: Theory, Application and Tools. IFIP AICT, pp. 435\u2013450. Springer, Berlin (1996). doi: 10.1007\/978-0-387-35079-0_28"},{"key":"51_CR15","doi-asserted-by":"crossref","unstructured":"Ben-Hafaiedh, I., Susanne, G., Jaber, M.: Model-based design and distributed implementation of bus arbiter for multiprocessors. In: IEEE ICECS, pp. 65\u201368 (2011)","DOI":"10.1109\/ICECS.2011.6122215"},{"key":"51_CR16","first-page":"25","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25\u201359 (1987)","journal-title":"Comput. Netw."},{"key":"51_CR17","unstructured":"Bliudze, S., Sifakis, J.: Algebraic semantics of hierarchical connectors in the BIP framework. Technical report, Verimag, February 2007"},{"issue":"2","key":"51_CR18","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10617-012-9091-0","volume":"17","author":"B Bonakdarpour","year":"2013","unstructured":"Bonakdarpour, B., Bozga, M., Quilbeuf, J.: Model-based implementation of distributed systems with priorities. Des. Autom. Embed. Syst. 17(2), 251\u2013276 (2013)","journal-title":"Des. Autom. Embed. Syst."},{"key":"51_CR19","doi-asserted-by":"crossref","unstructured":"Astefanoaei, L., Rayana, S.-B., Bensalem, S., Bozga, M., Combaz, J.: Compositional verification for timed systems based on automatic invariant generation. Log. Methods Comput. Sci. (LMCS) 11 (2015)","DOI":"10.2168\/LMCS-11(3:15)2015"},{"key":"51_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64\u201379. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-88387-6_7"},{"key":"51_CR21","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/MM.1984.291218","volume":"4","author":"D Taub","year":"1984","unstructured":"Taub, D.: Arbitration and control acquisition in the proposed ieee 896 futurebus. IEEE Micro 4, 28\u201341 (1984)","journal-title":"IEEE Micro"},{"key":"51_CR22","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/s00446-012-0168-6","volume":"25","author":"B Bonakdarpour","year":"2012","unstructured":"Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Distrib. Comput. 25, 383\u2013409 (2012)","journal-title":"Distrib. Comput."},{"key":"51_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-319-24953-7_25","volume-title":"Automated Technology for Verification and Analysis","author":"S Bliudze","year":"2015","unstructured":"Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326\u2013343. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-24953-7_25"},{"key":"51_CR24","doi-asserted-by":"crossref","unstructured":"Shin, E.S., Mooney, V.J., Riley, G.F.: Round robin arbiter design and generation. In: International Symposium on System Synthesis (2002)","DOI":"10.1145\/581199.581253"},{"issue":"6","key":"51_CR25","first-page":"2047","volume":"26","author":"J Jou","year":"2010","unstructured":"Jou, J., Lee, Y.: An optimal round-robin arbiter design for NoC. J. Inf. Sci. Eng. 26(6), 2047\u20132058 (2010)","journal-title":"J. Inf. Sci. Eng."},{"key":"51_CR26","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1017\/S096012951200028X","volume":"23","author":"T Abdellatif","year":"2013","unstructured":"Abdellatif, T., Combaz, J., Sifakis, J.: Rigorous implementation of real-time systems - from theory to application. Math. Struct. Comput. Sci. 23, 882\u2013914 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"7","key":"51_CR27","doi-asserted-by":"crossref","first-page":"1283","DOI":"10.1109\/TCAD.2006.888284","volume":"26","author":"S Murali","year":"2007","unstructured":"Murali, S., Benini, L., De Micheli, G.: An application-specific design methodology for on-chip crossbar generation. Comput.-Aided Des. Integr. Circ. Syst. 26(7), 1283\u20131296 (2007)","journal-title":"Comput.-Aided Des. Integr. Circ. Syst."},{"key":"51_CR28","doi-asserted-by":"crossref","unstructured":"Lahiri, K., Raghunathan, A., Lakshminarayana, G.: LOTTERYBUS: a new high performance communication architecture for system-on-chip designs. In: Design Automation Conference, pp. 15\u201320 (2001)","DOI":"10.1145\/378239.378252"}],"container-title":["Lecture Notes in Computer Science","Algorithms and Architectures for Parallel Processing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-49583-5_51","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T18:53:42Z","timestamp":1568573622000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-49583-5_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319495828","9783319495835"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-49583-5_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}