{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:03:42Z","timestamp":1725563022310},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642148071"},{"type":"electronic","value":"9783642148088"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14808-8_12","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T09:52:01Z","timestamp":1282384321000},"page":"168-183","source":"Crossref","is-referenced-by-count":0,"title":["Specification and Verification of a MPI Implementation for a MP-SoC"],"prefix":"10.1007","author":[{"given":"Umberto Souza","family":"da Costa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ivan Soares","family":"de Medeiros J\u00fanior","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcel Vinicius Medeiros","family":"Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1109\/DATE.2004.1268966","volume-title":"Conference on Design, Automation and Test in Europe","author":"M. Loghi","year":"2004","unstructured":"Loghi, M., Angiolini, F., Bertozzi, D., Benini, L., Zafalon, R.: Analyzing On-Chip Communication in a MPSoC Environment. In: Conference on Design, Automation and Test in Europe, pp. 752\u2013757. IEEE Computer Society, Washington (2004)"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/B978-012385251-9\/50014-1","volume-title":"Multiprocessor Systems-on-Chips","author":"A.A. Jerraya","year":"2005","unstructured":"Jerraya, A.A., Wolf, W.: The What, Why, and How of MPSoCs. In: Jerraya, A.A., Wolf, W. (eds.) Multiprocessor Systems-on-Chips, pp. 1\u201318. Morgan Kauffman, San Francisco (2005)"},{"key":"12_CR3","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1145\/1284480.1284558","volume-title":"20th annual conference on Integrated Circuits and Systems Design","author":"G. Gir\u00e3o","year":"2007","unstructured":"Gir\u00e3o, G., Oliveira, B.C., Soares, R., Silva, I.S.: Cache Coherency Communication Cost In A NoC-Based Mp-Soc Platform. In: 20th annual conference on Integrated Circuits and Systems Design, pp. 288\u2013293. ACM, New York (2007)"},{"key":"12_CR4","unstructured":"IEEE Comp. Society: IEEE Standard SystemC Language Reference Manual (2006)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1109\/2.976921","volume":"35","author":"L. Benini","year":"2002","unstructured":"Benini, L., De Micheli, G.: Networks on Chips: A New SoC Paradigm. Computer\u00a035, 70\u201378 (2002)","journal-title":"Computer"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1109\/SBCCI.2002.1137647","volume-title":"15th Symposium on Integrated Circuits and Systems Design","author":"C.A. Zeferino","year":"2002","unstructured":"Zeferino, C.A., Kreutz, M.E., Carro, L., Susin, A.A.: A Study on Communication Issues for Systems-on-Chip. In: 15th Symposium on Integrated Circuits and Systems Design, pp. 121\u2013126. IEEE Computer Society, Washington (2002)"},{"key":"12_CR7","volume-title":"MPI: The Complete Reference","author":"M. Snir","year":"1998","unstructured":"Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J.: MPI: The Complete Reference. The MIT Press, Massachusetts (1998)"},{"key":"12_CR8","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)"},{"key":"12_CR9","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1997","unstructured":"Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1997)"},{"key":"12_CR10","unstructured":"Formal Systems Ltd: Failures-Divergence Refinement. FDR2 User Manual (2005)"},{"key":"12_CR11","unstructured":"Oliveira, B.C.: Simula\u00e7\u00e3o de reservat\u00f3rios de petr\u00f3leo em ambiente MPSoC. Master\u2019s Dissertation, P\u00f3s-Gradua\u00e7\u00e3o em Sistemas e Computa\u00e7\u00e3o, UFRN (2009)"},{"key":"12_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0849-5","volume-title":"Concurrent Scientific Computing","author":"E.F. Velde Van de","year":"1994","unstructured":"Van de Velde, E.F.: Concurrent Scientific Computing. Springer, New York (1994)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-79707-4_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"R. Palmer","year":"2008","unstructured":"Palmer, R., Delisi, M., Gopalakrishnan, G., Kirby, R.M.: An Approach to Formalization and Analysis of Message Passing Libraries. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 164\u2013181. Springer, Heidelberg (2008)"},{"key":"12_CR14","series-title":"NATO Science Series F","first-page":"183","volume-title":"Calculational System Design","author":"L. Lamport","year":"1999","unstructured":"Lamport, L.: Specifying Concurrent Systems with TLA+. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO Science Series F, vol.\u00a0173, pp. 183\u2013247. IOS Press, Amsterdam (1999)"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1145\/1345206.1345257","volume-title":"13th Symposium on Principles and Practice of Parallel Programming","author":"G. Li","year":"2008","unstructured":"Li, G., Delisi, M., Gopalakrishnan, G., Kirby, R.M.: Formal specification of the MPI-2.0 standard in TLA+. In: 13th Symposium on Principles and Practice of Parallel Programming, pp. 283\u2013284. ACM Press, New York (2008)"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Avrunin, G.S.: Modeling MPI programs for verification. Technical report, Department of Computer Science, University of Massachusetts (2004)","DOI":"10.1145\/1065944.1065957"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-540-24732-6_20","volume-title":"Model Checking Software","author":"S.F. Siegel","year":"2004","unstructured":"Siegel, S.F., Avrunin, G.S.: Verification of MPI-Based Software for Scientific Computation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 286\u2013303. Springer, Heidelberg (2004)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-69738-1_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.F. Siegel","year":"2007","unstructured":"Siegel, S.F.: Model Checking Nonblocking MPI Programs. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 44\u201358. Springer, Heidelberg (2007)"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"1466","DOI":"10.1109\/CCECE.2006.277495","volume-title":"Canadian Conference on Electrical and Computer Engineering (CCECE)","author":"J.D. Carter","year":"2006","unstructured":"Carter, J.D., Gardner, W.B.: A Formal CSP Framework for Message-Passing HPC Programming. In: Canadian Conference on Electrical and Computer Engineering (CCECE), pp. 1466\u20131470. IEEE Computer Society, Washington (2006)"},{"key":"12_CR20","first-page":"379","volume-title":"Supercomputing Symposium","author":"G. Burns","year":"1994","unstructured":"Burns, G., Daoud, R., Vaigl, J.: LAM: An Open Cluster Environment for MPI. In: Supercomputing Symposium, pp. 379\u2013386. ACM Press, New York (1994)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-46017-9_16","volume-title":"Model Checking Software","author":"O.S. Matlin","year":"2002","unstructured":"Matlin, O.S., Lusk, E.L., McCune, W.: SPINning Parallel Systems Software. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 213\u2013220. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14808-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T23:03:45Z","timestamp":1685747025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14808-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642148071","9783642148088"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14808-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}