{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T18:19:32Z","timestamp":1694629172442},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2007,3,2]],"date-time":"2007-03-02T00:00:00Z","timestamp":1172793600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2007,3,2]],"date-time":"2007-03-02T00:00:00Z","timestamp":1172793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2007,6]]},"DOI":"10.1007\/s10009-007-0031-4","type":"journal-article","created":{"date-parts":[[2007,3,1]],"date-time":"2007-03-01T19:12:12Z","timestamp":1172776332000},"page":"371-391","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Checking safety properties on-the-fly with the sweep-line method"],"prefix":"10.1007","volume":"9","author":[{"given":"Guy Edward","family":"Gallasch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Billington","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Somsak","family":"Vanit-Anunchai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars Michael","family":"Kristensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,3,2]]},"reference":[{"key":"31_CR1","unstructured":"Barrett, W.A., Couch, J.D.: Compiler Construction: Theory and Practice. Science Research Associates (1979)"},{"key":"31_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification\u2014Model-Checking Techniques and Tools","author":"B. B\u00e9rard","year":"2001","unstructured":"B\u00e9rard B., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L. and Schnoebelen Ph. (2001). Systems and Software Verification\u2014Model-Checking Techniques and Tools. Springer, Heidelberg"},{"key":"31_CR3","unstructured":"Billington, J.: Abstract Specification of the ISO Transport Service Definition using Labelled Numerical Petri Nets. Protocol Specification, Testing, and Verification, vol. III. Elsevier, Amsterdam, pp. 173\u2013185 (1983)"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Billington, J., Gallasch, G.E., Han, B.: A coloured petri net approach to protocol verification. In: Lectures on Concurrency and Petri Nets, Advances in Petri Nets. Lecture Notes in Computer Science, vol. 3098. Springer, Heidelberg, pp. 210\u2013290 (2004)","DOI":"10.1007\/978-3-540-27755-2_6"},{"issue":"1","key":"31_CR5","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/TSMCA.2003.820582","volume":"34","author":"J. Billington","year":"2004","unstructured":"Billington J., Gallasch G.E., Kristensen L.M. and Mailund T. (2004). Exploiting equivalence reduction and the sweep-line method for detecting terminal states. IEEE Trans. Syst. Man and Cybernet. Part A: Syst. Humans 34(1): 23\u201337","journal-title":"IEEE Trans. Syst. Man and Cybernet. Part A: Syst. Humans"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers (1999)","DOI":"10.1007\/978-1-4757-4070-7"},{"key":"31_CR7","unstructured":"Christensen, S., Jensen, K., Kristensen, L.M.: Design\/CPN Occurrence Graph Manual. Department of Computer Science, University of Aarhus, Denmark. On-line version: http:\/\/www.daimi.au.dk\/designCPN\/"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Proceedings of TACAS 2001. Lecture Notes in Computer Science, vol. 2031. Springer, Heidelberg, pp 450\u2013464 (2001)","DOI":"10.1007\/3-540-45319-9_31"},{"key":"31_CR9","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press (2000)"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Proceedings of Formal Methods\u201999, Toulouse, France. Lecture Notes in Computer Science, vol. 1708. Springer, Heidelberg, pp. 253\u2013271 (1999)","DOI":"10.1007\/3-540-48119-2_16"},{"key":"31_CR11","unstructured":"CPN Tools: http:\/\/wiki.daimi.au.dk\/cpntools\/cpntools.wiki"},{"key":"31_CR12","unstructured":"Design\/CPN Online: http:\/\/www.daimi.au.dk\/designCPN\/"},{"key":"31_CR13","unstructured":"FSM Library, AT&T Research Labs: http:\/\/www.research. att.com\/sw\/tools\/fsm\/"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Gallasch, G.E., Han, B., Billington, J.: Sweep-line analysis of TCP connection management. In: Proceedings of the International Conference on Formal Engineering Methods (ICFEM\u201905). Lecture Notes in Computer Science, vol. 3785. Springer, Heidelberg, pp. 156\u2013172 (2005)","DOI":"10.1007\/11576280_12"},{"key":"31_CR15","unstructured":"Gallasch, G.E., Ouyang, C., Billington, J., Kristensen, L.M.: Experimenting with progress mappings for the sweep-line analysis of the internet open trading protocol. In: Fifth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. Department of Computer Science, University of Aarhus (2004). Available via http:\/\/www. daimi.au.dk\/CPnets\/workshop04\/cpn\/papers\/"},{"key":"31_CR16","unstructured":"Gallasch, G.E., Vanit-Anunchai, S., Billington, J., Kristensen, L.M.: Checking language inclusion on-the-fly with the sweep-line method. In: Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. Department of Computer Science, University of Aarhus (2005). Available via http:\/\/www.daimi.au.dk\/CPnets\/workshop05\/cpn\/papers\/"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing and Verification, XV. Chapman & Hall, UK, pp. 3\u201318 (1996)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Gordon, S., Kristensen, L.M., Billington, J.: Verification of a revised WAP wireless transaction protocol. In: Proceedings of 23rd International Conference on Application and Theory of Petri Nets. Lecture Notes in Computer Science, vol. 2360. Springer, Heidelberg, pp 182\u2013202 (2002)","DOI":"10.1007\/3-540-48068-4_12"},{"key":"31_CR19","unstructured":"Han, B.: Formal specification of the TCP service and verification of TCP connection management. PhD thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia, December 2004"},{"key":"31_CR20","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann G.J. (2003). The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading"},{"key":"31_CR21","unstructured":"ITU-T. Recommendation X.210, Information Technology\u2014Open Systems Interconnection\u2014Basic Reference Model: Conventions for the Definition of OSI Services. International Telecommunications Union, November 1993"},{"key":"31_CR22","unstructured":"ITU-T. Recommendation X.214, Information Technology\u2014Open Systems Interconnection\u2014Transport Service Definition. International Telecommunications Union, November 1995"},{"key":"31_CR23","unstructured":"Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Vol. 1, Basic Concepts, 2nd edn. Monographs in Theoretical Computer Science. Springer, Heidelberg (1997)"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Kohler, E., Handley, M., Floyd, S.: Datagram Congestion Control Protocol, RFC 4340. Available via http:\/\/www. rfc-editor.org\/rfc\/rfc4340.txt, March 2006","DOI":"10.17487\/rfc4340"},{"key":"31_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1844-9","volume-title":"Automata and Computability","author":"D.C. Kozen","year":"1997","unstructured":"Kozen D.C. (1997). Automata and Computability. Springer, Heidelberg"},{"issue":"2","key":"31_CR26","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/s100090050021","volume":"2","author":"L.M. Kristensen","year":"1998","unstructured":"Kristensen L.M., Christensen S. and Jensen K. (1998). The Practitioner\u2019s Guide to Coloured Petri Nets. Int. J. Softw. Tools Technol. Transf. 2(2): 98\u2013132","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"31_CR27","doi-asserted-by":"crossref","unstructured":"Kristensen, L.M., Mailund, T.: A compositional sweep-line state space exploration method. In: Proceedings of FORTE\u201902. Lecture Notes in Computer Science, vol. 2529. Springer, Heidelberg, pp. 327\u2013343 (2002)","DOI":"10.1007\/3-540-36135-9_21"},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"Kristensen, L.M., Mailund, T.: A Generalised sweep-line method for safety properties. In: Proceedings of FME\u201902. Lecture Notes in Computer Science, vol. 2391. Springer, Heidelberg, pp. 549\u2013567 (2002)","DOI":"10.1007\/3-540-45614-7_31"},{"key":"31_CR29","doi-asserted-by":"crossref","unstructured":"Kristensen, L.M., Mailund, T.: Efficient path finding with the sweep-line method using external storage. In: Proceedings of the International Conference on Formal Engineering Methods (ICFEM\u201903). Lecture Notes in Computer Science, vol. 2885. Springer, Heidelberg, pp 319\u2013337 (2003)","DOI":"10.1007\/978-3-540-39893-6_19"},{"key":"31_CR30","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman O. and Vardi M.Y. (2001). Model checking of safety properties. Formal Methods Syst. Des. 19: 291\u2013314","journal-title":"Formal Methods Syst. Des."},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of 12th ACM Symposium on Principles of Programming Languages, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"31_CR32","doi-asserted-by":"crossref","unstructured":"Mailund, T.: Analysing infinite-state systems by combining equivalence reduction and the sweep-line method. In: Proceedings of ICATPN\u201902. Lecture Notes in Computer Science, vol. 2360. Springer, Heidelberg, pp. 314\u2013334 (2002)","DOI":"10.1007\/3-540-48068-4_19"},{"key":"31_CR33","unstructured":"Mailund, T.: Sweeping the state space\u2014a sweep-line state space exploration method. PhD thesis, Department of Computer Science, University of Aarhus, February 2003"},{"key":"31_CR34","unstructured":"On-The-Fly, LTL Model Checking with SPIN. http:\/\/ spinroot.com"},{"key":"31_CR35","unstructured":"Ouyang, C.: Formal specification and verification of the internet open trading protocol using coloured petri nets. PhD thesis, Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, Adelaide, Australia, June 2004"},{"key":"31_CR36","doi-asserted-by":"crossref","unstructured":"Schmidt, K.: Automated generation of a progress measure for the sweep-line method. In: Proceedings of TACAS\u201904. Lecture Notes in Computer Science, vol. 2988. Springer, Heidelberg, pp 192\u2013204 (2004)","DOI":"10.1007\/978-3-540-24730-2_17"},{"key":"31_CR37","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The State Explosion Problem. In: Lectures on Petri Nets I: Basic Models. Lecture Notes in Computer Science, vol. 1491. Springer, Heidelberg, pp. 429\u2013528 (1998)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"31_CR38","unstructured":"Vanit-Anunchai, S., Billington, J.: Initial result of a formal analysis of dccp connection management. In: Proceedings of INC 2004, Plymouth, UK, pp. 63\u201370, July 2004"},{"key":"31_CR39","doi-asserted-by":"crossref","unstructured":"Vanit-Anunchai, S., Billington, J., Kongprakaiwoot, T.: Discovering chatter and incompleteness in the datagram congestion control protocol. In: Proceedings of FORTE\u201905. Lecture Notes in Computer Science, vol. 3731. Springer, Heidelberg, pp. 143\u2013158 (2005)","DOI":"10.1007\/11562436_12"},{"key":"31_CR40","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of 1st Symposium on Logic in Computer Science, Cambridge, USA. IEEE Computer Society Press, pp. 332\u2013344 (1986)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0031-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-007-0031-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0031-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-007-0031-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T01:50:51Z","timestamp":1652838651000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-007-0031-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,3,2]]},"references-count":40,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2007,6]]}},"alternative-id":["31"],"URL":"https:\/\/doi.org\/10.1007\/s10009-007-0031-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,3,2]]},"assertion":[{"value":"2 March 2007","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}