{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T17:10:10Z","timestamp":1739034610217,"version":"3.37.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,3,24]],"date-time":"2009-03-24T00:00:00Z","timestamp":1237852800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,7]]},"DOI":"10.1007\/s10009-009-0104-7","type":"journal-article","created":{"date-parts":[[2009,3,23]],"date-time":"2009-03-23T06:59:43Z","timestamp":1237791583000},"page":"217-238","source":"Crossref","is-referenced-by-count":2,"title":["System-on-chip design by proof-based refinement"],"prefix":"10.1007","volume":"11","author":[{"given":"Dominique","family":"Cansell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cyril","family":"Proch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,24]]},"reference":[{"key":"104_CR1","unstructured":"Abraham, D., Cansell, D., Ditsch, P., M\u00e9ry, D., Proch, C.: The challenge of QoS for digital television services. EBU Technical Review, April 2005"},{"key":"104_CR2","unstructured":"Abraham, D., Cansell, D., Ditsch, P., M\u00e9ry, D., Proch, C.: Synthesis of the QoS for digital TV services. In: IBC\u201905, The Netherlands (2005)"},{"key":"104_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book\u2014Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial J.-R.: The B Book\u2014Assigning Programs to Meanings. Cambridge University Press, London (1996) ISBN 0-521-49619-5"},{"key":"104_CR4","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Cansell, D.: Click\u2019n\u2019Prove: interactive proofs within set theory. In: David Basin et Burkhart Wolff (ed.) 16th International Conference on Theorem Proving in Higher Order Logics\u2014TPHOLs\u20192003, Rome.Lecture notes in Computer Science, vol. 2758, pp. 1\u201324. Springer, Heidelberg (2003)","DOI":"10.1007\/10930755_1"},{"issue":"3","key":"104_CR5","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/s001650300002","volume":"14","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial J.-R., Cansell D., M\u00e9ry D.: A mechanically proved and incremental development of IEEE 1394 tree identify protocol. Formal Asp. Comput. 14(3), 215\u2013227 (2003)","journal-title":"Formal Asp. Comput."},{"issue":"1","key":"104_CR6","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"R.J.R. Back","year":"1979","unstructured":"Back R.J.R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49\u201368 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"104_CR7","volume-title":"Hardware-Software Co-Design of Embedded Systems","author":"F. Balarin","year":"2000","unstructured":"Balarin F., Chiodo M., Giusto P., Hsieh H., Jurecska A., Lavagno L., Passerone C., Sangiovanni-Vincentelli A., Sentovich E., Suzuki K., Tabbara B.: Hardware-Software Co-Design of Embedded Systems. Kluwer, Dordrecht (2000)"},{"key":"104_CR8","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1098\/rsta.1992.0027","volume":"339","author":"G. Berry","year":"1992","unstructured":"Berry G.: Esterel on hardware. Philos. Trans. R. Soc. Lond. 339, 87\u2013104 (1992)","journal-title":"Philos. Trans. R. Soc. Lond."},{"issue":"2","key":"104_CR9","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry G., Gonthier G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"volume-title":"Logics of Specification Languages. EATCS Textbook in Computer Science","year":"2007","key":"104_CR10","unstructured":"Bj\u00f8rner, D., Henson, M.C. (eds.): Logics of Specification Languages. EATCS Textbook in Computer Science. Springer, Heidelberg (2007)"},{"key":"104_CR11","unstructured":"Cansell, D., Culat, J.-F., M\u00e9ry, D., Proch, C.: Derivation of SystemC code from abstract system models. In: Forum on specification & Design Languages\u2014FDL\u201904, Lille, France, September 2004"},{"key":"104_CR12","first-page":"33","volume-title":"The event-B Modelling Method: Concepts and Case Studies","author":"D. Cansell","year":"2007","unstructured":"Cansell D., M\u00e9ry D.: The event-B Modelling Method: Concepts and Case Studies, pp. 33\u2013140. Springer, Berlin (2007)"},{"key":"104_CR13","unstructured":"Cansell, D., M\u00e9ry, D., Proch, C.: Projet RNRT EQUAST SP2 sp\u00e9cification incr\u00e9mentale du syst\u00e8me. Rapport de recherche, LORIA, October 2004"},{"key":"104_CR14","unstructured":"Cansell, D., Tanougast, C., Berviller, Y., M\u00e9ry, D., Proch, C., Rabah, H., Weber, S.: Proof-based design of a microelectronic architecture for mpeg-2 bit-rate measurement. In: Forum on specification and Design Languages\u2014FDL\u201903, Frankfurt, Germany, September 2003"},{"key":"104_CR15","volume-title":"Parallel Program Design A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy K.M., Misra J.: Parallel Program Design A Foundation. Addison-Wesley, Reading (1988) ISBN 0-201-05866-9"},{"key":"104_CR16","unstructured":"Clarke E.M., Grumberg O., Peled D.A.: Model Checking. The MIT Press, (2000)"},{"key":"104_CR17","unstructured":"ClearSy. Web site B4free set of tools for development of B models. http:\/\/www.b4free.com\/index.php (2004)"},{"key":"104_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Proc. Int. Symp. on Verification\u2014Theory & Practice\u2014Honoring Zohar Manna\u2019s 64th Birthday, pp. 243\u2013268. Taormina, Italy, June 29\u2013July 4 2003","DOI":"10.1007\/978-3-540-39910-0_11"},{"key":"104_CR19","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"104_CR20","unstructured":"European Broadcasting Union. Digital video broadcasting (DVB)- measurement guidelines for DVB systems. Technical Report TR 101 290 v1.2.1., ETSI, 05 (2001)"},{"key":"104_CR21","unstructured":"Gawanmeh, A., Habibi, A., Tahar, S.: An executable operational semantics for SystemC using Abstract State Machines. Technical report, Concordia University, Department of Electrical and Computer Engineering, March 2005"},{"key":"104_CR22","volume-title":"Formal Semantics for VHDL","author":"U. Gl\u00e4sser","year":"1995","unstructured":"Gl\u00e4sser U., B\u00f6rger E., M\u00fcller W.: Formal definition of an abstract VHDL\u201993 simulator by EA-machines. In: DelgadoKloos, C., Breuer, P.T. (eds) Formal Semantics for VHDL, Kluwer, Dordrecht (1995)"},{"key":"104_CR23","unstructured":"Hardware Verification Group. Hands-on Manual to FormalCheck, Version 2.3. Concordia University, Montreal (2000)"},{"key":"104_CR24","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.entcs.2005.01.021","volume":"131","author":"A. Habibi","year":"2005","unstructured":"Habibi A., Tahar S.: On the transformation of systemc to asml using abstract interpretation. Electron. Notes Theor. Comput. Sci. 131, 39\u201349 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"104_CR25","doi-asserted-by":"crossref","unstructured":"Holmstr\u00f6m, S., Sere, K.: Reconfigurable hardware\u2014a case study in codesign. In: FPL: From FPGAs to Computing Paradigm. Lecture Notes in Computer Science, vol. 1482, pp. 451\u2013455. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055279"},{"key":"104_CR26","unstructured":"IEEE Std1076-1993. Standard VHDL Langage Reference Manual. IEEE (1993)"},{"key":"104_CR27","unstructured":"Moy, M.: Techniques and Tools for the verification of Systems-on-a-Chip at the Transaction Level. PhD thesis, Institut National Polytechnique de Grenoble, December 2005"},{"key":"104_CR28","doi-asserted-by":"crossref","unstructured":"Moy, M., Maraninchi, F., Maillet-Contoz, L.: LusSy: A toolbox for the analysis of systems-on-a-chip at the transactional level. In: International Conference on Application of Concurrency to System Design, Juin 2005","DOI":"10.1109\/ACSD.2005.23"},{"key":"104_CR29","doi-asserted-by":"crossref","unstructured":"Moy, M., Maraninchi, F., Maillet-Contoz, L.: Pinapa: An extraction tool for SystemC descriptions of systems-on-a-chip. In: ACM International Conference on Embedded Software (EMSOFT\u201905), Jersey city, September 2005","DOI":"10.1145\/1086228.1086286"},{"key":"104_CR30","doi-asserted-by":"crossref","unstructured":"Mueller, W., D\u00f6mer, R., Gerstlauer, A.: The formal execution semantics of SpecC. In: ISSS \u201902: Proceedings of the 15th international symposium on System Synthesis, pp. 150\u2013155. ACM Press, New York (2002)","DOI":"10.1145\/581199.581234"},{"key":"104_CR31","unstructured":"Open SystemC Initiative. SystemC 2.0.1 Language Reference Manual (2004)"},{"key":"104_CR32","unstructured":"Pasricha, S.: Transaction level modeling of SoC in SystemC 2.0. Technical report, STMicroelectronics Ltd (2002)"},{"key":"104_CR33","doi-asserted-by":"crossref","unstructured":"Plosila, J., Sere, K.: Action systems in pipelined processor design. In: Third International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC \u201997), pp. 156\u2013166. IEEE Computer Society, Eindhoven, The Netherlands, 7\u201310 April 1997","DOI":"10.1109\/ASYNC.1997.587171"},{"issue":"1","key":"104_CR34","first-page":"89","volume":"7","author":"J. Ruf","year":"2001","unstructured":"Ruf J.: RAVEN: Real-time analyzing and verification environment. J. Univ. Comput. Sci. 7(1), 89\u2013104 (2001)","journal-title":"J. Univ. Comput. Sci."},{"key":"104_CR35","unstructured":"Ruf, J., Hoffmann, D., Gerlach, J., Kropf, T., Rosenstiehl, W., Mueller, W.: The simulation semantics of SystemC. In: DATE \u201901: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 64\u201370. IEEE Press, Piscataway (2001)"},{"key":"104_CR36","doi-asserted-by":"crossref","unstructured":"Ruf, J., Hoffmann, D., Kropf, T., Rosenstiel, W.: Simulation-guided property checking based on a multi-valued AR-automata. In: DATE \u201901: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 742\u2013748. IEEE Press, Piscataway (2001)","DOI":"10.1109\/DATE.2001.915111"},{"key":"104_CR37","doi-asserted-by":"crossref","unstructured":"Salem, A.: Formal semantics of synchronous SystemC. In DATE \u201903: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 376\u2013381. IEEE Computer Society, Washington (2003)","DOI":"10.1109\/DATE.2003.1253637"},{"key":"104_CR38","unstructured":"SOCFV Project. System on chip formal verification home page. http:\/\/www.ensta.fr\/~hammami\/resproj.SOCFV.html (2004)"},{"key":"104_CR39","unstructured":"Synopsys Inc. Describing synthesizable RTL in SystemC. Technical report, Synopsys, November 2002"},{"key":"104_CR40","doi-asserted-by":"crossref","unstructured":"Talpin, J.-P., Le Guernic, P., Shukla, S.K., Gupta, R.K., Doucet, F.: Polychrony for formal refinement-checking in a system-level design methodology. In: 3rd International Conference on Application of Concurrency to System Design (ACSD 2003), pp. 9\u201319. IEEE Computer Society, Guimaraes, 18\u201320 June 2003","DOI":"10.1109\/CSD.2003.1207695"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0104-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0104-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0104-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T16:38:37Z","timestamp":1739032717000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0104-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,24]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,7]]}},"alternative-id":["104"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0104-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2009,3,24]]}}}