{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:40:31Z","timestamp":1737592831566,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_32","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"557-574","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Visualizing System Factorizations with Behavior Tables"],"prefix":"10.1007","author":[{"given":"Alex","family":"Tsow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven D.","family":"Johnson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"32_CR1","unstructured":"Bhaskar Bose. DDD-FM9001: Derivation of a Verified Microprocessor. PhD thesis, Computer Science Department, Indiana University, USA, 1994. Technical Report No. 456, 155 pages, ftp:\/\/ftp.cs.indiana.edu\/pub\/techreports\/TR456.ps.Z ."},{"key":"32_CR2","unstructured":"Robert G. Burger. The scheme machine. Technical Report 413, Indiana University, Computer Science Department, August 1994. 59 pages."},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Constance Heitmeyer, Alan Bull, Carolyn Gasarch, and Bruce Labaw. SCR*: a toolset for specifying and analyzing requirements. In Proceedings of the Tenth Annual Conference on Computer Assurance (COMPASS\u2019 95), pages 109\u2013122, 1995.","DOI":"10.21236\/ADA465318"},{"key":"32_CR4","unstructured":"D. N. Hoover, David Guaspari, and Polar Humenn. Applications of formal methods to specification and safety of avionics software. Contractor Report 4723, National Aeronautics and Space Administration Langley Research Center (NASA\/LRC), Hampton VA 23681-0001, November 1994."},{"key":"32_CR5","series-title":"Lect Notes Comput Sci","first-page":"260","volume-title":"Manipulating logical organization with system factorizations","author":"S. D. Johnson","year":"1989","unstructured":"Steven D. Johnson. Manipulating logical organization with system factorizations. In Leeser and Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of LNCS, pages 260\u2013281. Springer, July 1989."},{"key":"32_CR6","unstructured":"Steven D. Johnson. A tabular language for system design. In C. Michael Holloway and Kelly J. Hayhurst, editors, Lfm97: Fourth NASA Langley For-mal Methods Workshop, September 1997. NASA Conference Publication 3356, http:\/\/atb-www.larc.nasa.gov\/Lfm97\/ ."},{"key":"32_CR7","unstructured":"Steven D. Johnson and Bhaskar Bose. A system for mechanized digital design derivation. In IFIP and ACM\/SIGDA International Workshop on Formal Meth-ods in VLSI Design, 1991. Available as Indiana University Computer Science Department Technical Report No. 323 (rev. 1997)."},{"key":"32_CR8","unstructured":"Steven D. Johnson and Alex Tsow. Algebra of behavior tables. In C. M. Holloway, editor, Lfm2000. Langley Formal Methods Group, NASA, 2000. Proceedings of the 5th NASA Langley Formal Methods Workshop, Williamsburg, Virginia, 13\u201315 June, 2000, http:\/\/shemesh.larc.nasa.gov\/fm\/Lfm2000\/ ."},{"key":"32_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/BFb0031817","volume-title":"Formal Methods in Computer Aided Design","author":"R. Kumar","year":"1996","unstructured":"Ramayya Kumar, Christian Blumenr\u00f6ohr, Dirk Eisenbiegler, and Detlef Schmid. Formal synthesis in circuit design-a classification and survey. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer Aided Design, pages 294\u2013309, Berlin, 1996. Springer LNCS 1166. Proceedings of FMCAD\u201996."},{"issue":"9","key":"32_CR10","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N. G. Leveson","year":"1994","unstructured":"Nancy G. Leveson, Mats Per Erik Heimdahl, Holly Hildreth, and Jon Damon Reese. Requirements specifiation for process-control systems. IEEE Transactions on Software Engineering, 20(9):684\u2013707, September 1994.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"32_CR11","series-title":"Technical Report","volume-title":"PVS","author":"S. Owre","year":"1995","unstructured":"Sam Owre, John Rushby, and Natarajan Shankar. Analyzing tabular and state-transition specifications in PVS. Technical Report SRI-CSL-95-12, Computer Science Laboratory, SRI International, Menlo Park, CA, July 1995. Revised May 1996. Available, with specification files, from http:\/\/www.csl.sri.com\/csl-95-12.html ."},{"key":"32_CR12","unstructured":"Franklin P. Prosser and David E. Winkel. The Art of Digital Design. Prentice\/Hall International, second edition, 1987."},{"key":"32_CR13","unstructured":"Kamlesh Rath. Sequential System Decomposition. PhD thesis, Computer Science Department, Indiana University, USA, 1995. Technical Report No. 457, 90 pages."},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. Behavior tables: A basis for system representation and transformational system synthesis. In Proceedings of the International Conference on Computer Aided Design (ICCAD), pages 736\u2013740. IEEE, November 1993.","DOI":"10.1109\/ICCAD.1993.580170"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"M. Esen Tuna, Kamlesh Rath, and Steven D. Johnson. Specification and synthesis of bounded indirection. In Proceedings of the Fifth Great Lakes Symposium on VLSI (GLSVLSI95), pages 86\u201389. IEEE, March 1995.","DOI":"10.1109\/GLSV.1995.516030"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:23:52Z","timestamp":1737591832000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_32","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}