{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:41:49Z","timestamp":1725748909843},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410093"},{"type":"electronic","value":"9783642410109"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41010-9_8","type":"book-chapter","created":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T05:31:39Z","timestamp":1379309499000},"page":"108-122","source":"Crossref","is-referenced-by-count":5,"title":["Formal Analysis of the ACE Specification for Cache Coherent Systems-on-Chip"],"prefix":"10.1007","author":[{"given":"Abderahman","family":"Kriouile","sequence":"first","affiliation":[]},{"given":"Wendelin","family":"Serwe","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"ARM. AMBA AXI and ACE Protocol Specification, version ARM IHI 0022E (February 2013), \n                  \n                    http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ihi0022e","key":"8_CR1"},{"unstructured":"ARM. CoreLink CCI-400 Cache Coherent Interconnect: Technical Reference Manual, revision r1p1 (November 2012), \n                  \n                    http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ddi0470g\/DDI0470G_cci400_r1p1_trm.pdf","key":"8_CR2"},{"unstructured":"Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference manual of the LOTOS NT to LOTOS translator (version 5.8). INRIA\/VASY, 155 pages (March 2013)","key":"8_CR3"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-30232-2_16","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"G. Chehaibar","year":"2004","unstructured":"Chehaibar, G.: Integrating formal verification with Mur\u03c6 of distributed cache coherence protocols in FAME multiprocessor system design. In: de Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol.\u00a03235, pp. 243\u2013258. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Chen, M., Qin, X., Koo, H.-M., Mishra, P.: System-Level Validation: High-Level Modeling and Directed Test Generation Techniques. Springer (2013)","key":"8_CR5","DOI":"10.1007\/978-1-4614-1359-2"},{"issue":"1","key":"8_CR6","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-010-0092-y","volume":"36","author":"X. Chen","year":"2010","unstructured":"Chen, X., Yang, Y., Gopalakrishnan, G., Chou, C.-T.: Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. Formal Methods in System Design\u00a036(1), 37\u201364 (2010)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"8_CR7","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the Futurebus+ cache coherence protocol. Formal Methods in System Design\u00a06(2), 217\u2013232 (1995)","journal-title":"Formal Methods in System Design"},{"unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proc. of the Int.\u00a0Conf. on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525. IEEE (October 1992)","key":"8_CR8"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-60045-0_63","volume-title":"Computer Aided Verification","author":"A.T. Eir\u00edksson","year":"1995","unstructured":"Eir\u00edksson, A.T., McMillan, K.L.: Using Formal Verification\/Analysis Methods on the Critical Path in System Design: A Case Study. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 367\u2013380. Springer, Heidelberg (1995)"},{"issue":"2","key":"8_CR10","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H. Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2011: A toolbox for the construction and analysis of distributed processes. Software Tools for Technology Transfer\u00a015(2), 89\u2013107 (2013)","journal-title":"Software Tools for Technology Transfer"},{"doi-asserted-by":"crossref","unstructured":"Kahlouche, H., Viho, C., Zendri, M.: An industrial experiment in automatic generation of executable test suites for a cache coherency protocol. In: Proc. of the Int.\u00a0Workshop on Testing of Communicating Systems. Chapman&Hall (1998)","key":"8_CR11","DOI":"10.1007\/978-0-387-35381-4_13"},{"doi-asserted-by":"crossref","unstructured":"Kapoor, H.K., Kanakala, P., Verma, M., Das, S.: Design and formal verification of a hierarchical cache coherence protocol for NoC based multiprocessors. The Journal of Supercomputing (2013)","key":"8_CR12","DOI":"10.1007\/s11227-012-0865-8"},{"issue":"2","key":"8_CR13","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C. Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.R.: Formal Verification in Hardware Design: A Survey. ACM Trans. on Design Automation of Electronic Systems\u00a04(2), 123\u2013193 (1999)","journal-title":"ACM Trans. on Design Automation of Electronic Systems"},{"issue":"7","key":"8_CR14","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1145\/2209249.2209269","volume":"55","author":"M.M.K. Martin","year":"2012","unstructured":"Martin, M.M.K., Hill, M.D., Sorin, D.J.: Why On-Chip Cache Coherence Is Here to Stay. Communications of the ACM\u00a055(7), 78\u201389 (2012)","journal-title":"Communications of the ACM"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-68237-0_12","volume-title":"FM 2008: Formal Methods","author":"R. Mateescu","year":"2008","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 148\u2013164. Springer, Heidelberg (2008)"},{"unstructured":"McMillan, K.L., Schwalbe: Formal Verification of the Encore Gigamax cache consistency protocol. In: Proc. of the Int.\u00a0Symposium on Shared Memory Multiprocessors, pp. 242\u2013251 (1991)","key":"8_CR16"},{"issue":"1","key":"8_CR17","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F. Pong","year":"1997","unstructured":"Pong, F., Dubois, M.: Verification Techniques for Cache Coherence Protocols. ACM Computing Surveys\u00a029(1), 82\u2013126 (1997)","journal-title":"ACM Computing Surveys"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BFb0020472","volume-title":"EURO-PAR \u201995: Parallel Processing","author":"F. Pong","year":"1995","unstructured":"Pong, F., Nowatzyk, A., Aybay, G., Dubois, M.: Verifying Distributed Directory-based Cache Coherence Protocols: S3.mp, a Case Study. In: Haridi, S., Ali, K., Magnusson, P. (eds.) Euro-Par 1995. LNCS, vol.\u00a0966, pp. 287\u2013300. Springer, Heidelberg (1995)"},{"unstructured":"Ranjan, R.: Formal Techniques for Protocol Verification: A Case Study On Verifying the ARM ACE Protocol. In: Electronic Design (January 2012)","key":"8_CR19"},{"doi-asserted-by":"crossref","unstructured":"Slobodov\u00e1, A., Davis, J., Swords, S., Hunt Jr., W.: A Flexible Formal Verification Framework for Industrial Scale Verification. In: Proc. of the Int.\u00a0Conf. on Formal Methods and Models for Codesign, pp. 89\u201397 (July 2011)","key":"8_CR20","DOI":"10.1109\/MEMCOD.2011.5970515"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-60385-9_2","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Automatic Verification of the SCI Cache Coherence Protocol. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 21\u201334. Springer, Heidelberg (1995)"},{"unstructured":"Stevens, A.: Introduction to AMBA 4 ACE. ARM whitepaper (June 2011)","key":"8_CR22"},{"unstructured":"Thompson, C.: Verifying Cache Coherency Protocols with Verification IP. Synopsis (October 2012)","key":"8_CR23"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41010-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:06:08Z","timestamp":1558303568000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41010-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410093","9783642410109"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41010-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}