{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:23:39Z","timestamp":1694622219325},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2003,4,1]],"date-time":"2003-04-01T00:00:00Z","timestamp":1049155200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2003,4]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>This case study contains a formal verification of the IEEE 1394 FireWire tree identify protocol. Crucial properties of finite models of the protocol have been validated with state-of-the-art symbolic model checkers. Various optimisation techniques were applied to verify concrete and generic configurations.<\/jats:p>","DOI":"10.1007\/s001650300005","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"267-280","source":"Crossref","is-referenced-by-count":5,"title":["Verifying the IEEE 1394 FireWire Tree Identify Protocol with SMV"],"prefix":"10.1145","volume":"14","author":[{"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[{"name":"Department of Computer Science, Swiss Federal Institute of Technology, Zurich, Switzerland, , , , , , CH"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Swiss Federal Institute of Technology, Zurich, Switzerland, , , , , , CH"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"Proceedings of the 38th Conference on Design Automation","author":"Ben","year":"2001"},{"key":"p_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification: Model-Checking Techniques and Tools","author":"Berard B.","year":"2001"},{"key":"p_3","volume-title":"(editors","author":"Berry G","year":"2001"},{"key":"p_4","volume-title":"Proceedings of the 36th Design Automation Conference","author":"Biere A.","year":"1999"},{"key":"p_5","volume-title":"Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Biere A.","year":"1999"},{"key":"p_6","first-page":"454","volume-title":"Finding bugs in an alpha microprocessor using satisfiability solvers. In [BCF01]","author":"Bjesse P."},{"key":"p_7","unstructured":"[Bor97] Bor\u00e4lv A.: The industrial success of verification tools based on St\u00e5lmarck's method. In [Gru97]."},{"key":"p_8","first-page":"677","article-title":"Graph-based algorithms for Boolean function manipulation","author":"Bry","year":"1986","journal-title":"IEEE Transactions on Computers, 8(C-35)"},{"issue":"40","key":"p_9","first-page":"205","article-title":"On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication","volume":"2","author":"Bry","year":"1991","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"p_10","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch J. R.","year":"1992","journal-title":"Information and Computation"},{"key":"p_11","unstructured":"[Cad] Cadence SMV. Available at http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/."},{"key":"p_12","first-page":"9","volume-title":"Using SPIN to analyse the FireWire protocol: a case study. In [MRS01]","author":"Ca"},{"key":"p_13","volume-title":"Proceedings of the International Conference on Computer Design","author":"Campos S.","year":"1995"},{"key":"p_14","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification","author":"Cimatti A.","year":"2002"},{"key":"p_15","first-page":"52","volume-title":"Proceedings of the Workshop on Logics of Programs","author":"Cl","year":"1981"},{"key":"p_16","first-page":"450","volume-title":"Exploiting symmetry in temporal logic model checking. In [Cou93]","author":"Clarke E. M."},{"key":"p_17","volume-title":"Proceedings of the 11th International Symposium on Computer Hardware Description Languages and their Applications","author":"Clarke E. M.","year":"1993"},{"key":"p_18","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999"},{"key":"p_19","first-page":"436","volume-title":"Benefits of bounded model checking at an industrial setting. In [BCF01]","author":"Copty F."},{"key":"p_20","volume-title":"Heraklion, Greece, 28 June-1","author":"Cou","year":"1993"},{"key":"p_21","volume-title":"Proceedings of the Second Workshop on Formal Methods in Software Practice","author":"Dwyer M. B.","year":"1998"},{"key":"p_22","first-page":"522","volume-title":"Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE Computer Society","author":"Dill D. L."},{"key":"p_23","volume-title":"Handbook of Theoretical Computer Science","author":"Eme"},{"key":"p_24","first-page":"463","volume-title":"Symmetry and model checking. In [Cou93]","author":"Em"},{"key":"p_25","volume-title":"(editors","author":"Em","year":"2000"},{"key":"p_26","first-page":"1997","article-title":"Proceedings of the 9th International Conference on Computer Aided Verification, Haifa","volume":"22","author":"Gru","year":"1997","journal-title":"Israel"},{"key":"p_27","volume-title":": Design and Validation of Computer Protocols","author":"Hol","year":"1991"},{"key":"p_28","volume-title":"Institute of Electrical and Electronics Engineers","year":"1995"},{"key":"p_29","volume-title":"Institute of Electrical and Electronics Engineers","year":"2000"},{"issue":"9","key":"p_30","first-page":"41","article-title":"Better verification through symmetry","volume":"1","author":"Ip","year":"1996","journal-title":"Formal Methods in System Design"},{"key":"p_31","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann M.","year":"2000"},{"key":"p_32","volume-title":"(editors","author":"Maharaj S.","year":"2001"},{"issue":"3","key":"p_33","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/s001650300001","article-title":"The IEEE 1394 tree identify protocol","volume":"14","author":"Maharaj S.","year":"2003","journal-title":"Formal Aspects of Computing"},{"key":"p_34","volume-title":": Symbolic Model Checking","author":"Mc","year":"1993"},{"key":"p_35","volume-title":"Proceedings of the Fifth International Symposium on Programming","author":"Qu","year":"1982"},{"key":"p_36","first-page":"25","volume-title":"False loop detection in the IEEE 1394 tree identify phase. In [MRS01]","author":"Rom"},{"key":"p_37","volume-title":": Automated Theorem Proving in Software Engineering","author":"Sch","year":"2001"},{"key":"p_38","first-page":"31","volume-title":"A simple verification of the tree identify protocol with SMV. In [MRS01]","author":"Sc"},{"key":"p_39","first-page":"480","volume-title":"Tuning SAT checkers for bounded model checking. In [EmS00]","author":"Sht"},{"issue":"3","key":"p_40","first-page":"469","article-title":": Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k","volume":"4","author":"Si","year":"2001","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"p_41","unstructured":"[SMV] The SMV system. Available at http:\/\/www.cs.cmu.edu\/~modelcheck\/smv.html."},{"issue":"19","key":"p_42","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1023\/A:1011236117591","article-title":"Software engineering with formal methods: the development of a storm surge barrier control system: revisiting seven myths of formal methods","volume":"2","author":"Tretmans J.","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"p_43","unstructured":"[URL] http:\/\/www.inf.ethz.ch\/personal\/schuppan\/firewire."},{"key":"p_44","unstructured":"[Yan] Yang B.: SMV 2.4b. Available at http:\/\/www.cs.cmu.edu\/~bwolen\/software\/smv\/."},{"key":"p_45","unstructured":"[Zha97] Zhang H.: SATO: An efficient propositional prover. In [Gru97]."},{"key":"p_46","first-page":"279","volume-title":"Proceedings of the 2001 International Conference on Computer-Aided Design","author":"Zhang L.","year":"2001"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650300005.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650300005\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650300005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:41:55Z","timestamp":1641483715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650300005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,4]]},"references-count":46,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,4]]}},"alternative-id":["10.1007\/s001650300005"],"URL":"https:\/\/doi.org\/10.1007\/s001650300005","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,4]]}}}