乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,7]],"date-time":"2024-06-07T06:02:00Z","timestamp":1717740120060},"reference-count":42,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2005,11,1]],"date-time":"2005-11-01T00:00:00Z","timestamp":1130803200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":2851,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Journal of Logic and Algebraic Programming"],"published-print":{"date-parts":[[2005,11]]},"DOI":"10.1016\/j.jlap.2005.05.001","type":"journal-article","created":{"date-parts":[[2005,8,9]],"date-time":"2005-08-09T12:25:53Z","timestamp":1123590353000},"page":"51-104","source":"Crossref","is-referenced-by-count":21,"title":["Analyzing a \u03c7 model of a turntable system using Spin, CADP and Uppaal"],"prefix":"10.1016","volume":"65","author":[{"given":"E.","family":"Bortnik","sequence":"first","affiliation":[]},{"given":"N.","family":"Tr\u010dka","sequence":"additional","affiliation":[]},{"given":"A.J.","family":"Wijs","sequence":"additional","affiliation":[]},{"given":"B.","family":"Luttik","sequence":"additional","affiliation":[]},{"given":"J.M.","family":"van de Mortel-Fronczak","sequence":"additional","affiliation":[]},{"given":"J.C.M.","family":"Baeten","sequence":"additional","affiliation":[]},{"given":"W.J.","family":"Fokkink","sequence":"additional","affiliation":[]},{"given":"J.E.","family":"Rooda","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"1\u20133","key":"10.1016\/j.jlap.2005.05.001_bib1","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/S0304-3975(02)00334-1","article-title":"The power of reachability testing for timed automata","volume":"300","author":"Aceto","year":"2003","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.jlap.2005.05.001_bib2","unstructured":"R. Alur, C. Courcoubetis, D. Dill, Model checking in dense real-time, in: Proceedings of the 5th IEEE Symposium on Logic in Computer Science, LICS, 1990."},{"key":"10.1016\/j.jlap.2005.05.001_bib3","unstructured":"A.T. Hofkamp, H.W.A.M. van Rooy, Embedded Systems Laboratory Exercises Manual, 2003."},{"key":"10.1016\/j.jlap.2005.05.001_bib4","article-title":"Process Algebra","volume":"vol. 18","author":"Baeten","year":"1990"},{"key":"10.1016\/j.jlap.2005.05.001_bib5","unstructured":"D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers, Syntax and Consistent Equation Semantics of Hybrid Chi, CS-Report 04-37, Eindhoven University of Technology, 2004."},{"key":"10.1016\/j.jlap.2005.05.001_bib6","unstructured":"D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers, Syntax and Semantics of Timed Chi, CS-Report 05-09, Eindhoven University of Technology, 2005."},{"key":"10.1016\/j.jlap.2005.05.001_bib7","unstructured":"D.A. van Beek, A. van der Ham, J.E. Rooda, Modelling and control of process industry batch production systems, in: 15th Triennial World Congress of the International Federation of Automatic Control, Barcelona, Spain, CD-ROM, 2002."},{"issue":"1\u20133","key":"10.1016\/j.jlap.2005.05.001_bib8","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","article-title":"Process algebra for synchronous communication","volume":"60","author":"Bergstra","year":"1984","journal-title":"Inform. Control"},{"key":"10.1016\/j.jlap.2005.05.001_bib9","doi-asserted-by":"crossref","unstructured":"M. Bezem, J.F. Groote, Invariants in process algebra with data, in: CONCUR\u201994: Concurrency Theory, Lecture Notes in Computer Science, vol. 836, 1994, pp. 401\u2013416.","DOI":"10.1007\/978-3-540-48654-1_30"},{"key":"10.1016\/j.jlap.2005.05.001_bib10","unstructured":"S.C.C. Blom, W.J. Fokkink, J.F. Groote, I. van Langevelde, B. Lisser, J.C. van de Pol, \u03bcCRL: a toolset for analysing algebraic specifications, in: Proceedings of the 13th Conference on Computer Aided Verification (CAV2001), Lecture Notes in Computer Science, vol. 2102, 2001, pp. 250\u2013254."},{"key":"10.1016\/j.jlap.2005.05.001_bib11","unstructured":"S.C.C. Blom, N. Ioustinova, N. Sidorova, Timed verification with \u03bcCRL, in: Andrei Ershov Fifth International Conference Perspectives of System Informatics, Lecture Notes in Computer Science, vol. 2890, 2003, pp. 178\u2013192."},{"key":"10.1016\/j.jlap.2005.05.001_bib12","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/S0736-5845(00)00027-2","article-title":"Automatic verification of a manufacturing system","volume":"17","author":"Bos","year":"2001","journal-title":"Robot. Comput. Integrat. Manufactur."},{"key":"10.1016\/j.jlap.2005.05.001_bib13","unstructured":"V. Bos, J.J.T. Klein, Formal specification and analysis of industrial systems, Ph.D. thesis, Eindhoven University of Technology, 2002."},{"key":"10.1016\/j.jlap.2005.05.001_bib14","unstructured":"D. Bo\u0161na\u010dki, Enhancing state space reduction techniques for model checking, Ph.D. thesis, Eindhoven University of Technology, 2001."},{"key":"10.1016\/j.jlap.2005.05.001_bib15","series-title":"A Discipline of Programming","author":"Dijkstra","year":"1976"},{"key":"10.1016\/j.jlap.2005.05.001_bib16","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, M. Sighireanu, CADP\u2014a protocol validation and verification toolbox, in: Proceedings of the 8th Conference on Computer Aided Verification (CAV\u201996), Lecture Notes in Computer Science, vol. 1102, 1996, pp. 437\u2013440."},{"key":"10.1016\/j.jlap.2005.05.001_bib17","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04293-9","article-title":"Introduction to process algebra","author":"Fokkink","year":"2000"},{"key":"10.1016\/j.jlap.2005.05.001_bib18","doi-asserted-by":"crossref","unstructured":"W.J. Fokkink, J.F. Groote, J. Pang, B. Badban, J.C. van de Pol, Verifying a sliding window protocol in \u03bcCRL, in: Proceedings of the 10th Conference on Algebraic Methodology and Software Technology (AMAST\u201904), Lecture Notes in Computer Science, vol. 3116, 2004, pp. 148\u2013163.","DOI":"10.1007\/978-3-540-27815-3_15"},{"key":"10.1016\/j.jlap.2005.05.001_bib19","unstructured":"W.J. Fokkink, J.F. Groote, M. Reniers, Modelling distributed systems, Unpublished manuscript, 2002."},{"key":"10.1016\/j.jlap.2005.05.001_bib20","doi-asserted-by":"crossref","unstructured":"H. Garavel, H. Hermanns, On combining functional verification and performance evaluation using CADP, in: Proceedings of the 11th International Symposium of Formal Methods Europe (FME\u20192002), Lecture Notes in Computer Science, vol. 2391, 2002, pp. 410\u2013429.","DOI":"10.1007\/3-540-45614-7_23"},{"key":"10.1016\/j.jlap.2005.05.001_bib21","unstructured":"R. Gerth, Concise Promela Reference. Available from: ."},{"key":"10.1016\/j.jlap.2005.05.001_bib22","unstructured":"P. Godefroid, P. Wolper, Using partial orders for the efficient verification of deadlock freedom and safety properties, in: Proceedings of the 3rd Workshop on Computer-Aided Verification (CAV\u201991), Lecture Notes in Computer Science, vol. 575, 1991, pp. 410\u2013429."},{"key":"10.1016\/j.jlap.2005.05.001_bib23","unstructured":"J.F. Groote, The Syntax and Semantics of Timed \u03bcCRL, Technical Report SEN-R9709, CWI, Amsterdam, 1997."},{"key":"10.1016\/j.jlap.2005.05.001_bib24","doi-asserted-by":"crossref","unstructured":"J.F. Groote, F. Monin, J.C. van de Pol, Checking verifications of protocols and distributed systems by computer, in: Proceedings of the 9th Conference on Concurrency Theory (CONCUR\u201998), Lecture Notes in Computer Science, vol. 1466, 1998, pp. 629\u2013655.","DOI":"10.1007\/BFb0055652"},{"key":"10.1016\/j.jlap.2005.05.001_bib25","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"issue":"5","key":"10.1016\/j.jlap.2005.05.001_bib26","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker spin","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.jlap.2005.05.001_bib27","series-title":"The SPIN Model Checker","author":"Holzmann","year":"2003"},{"key":"10.1016\/j.jlap.2005.05.001_bib28","doi-asserted-by":"crossref","unstructured":"H.E. Jensen, K.G. Larsen, A. Skou, Modelling and analysis of a collision avoidance protocol using SPIN and Uppaal, in: Proceedings of the 2nd SPIN Workshop, Rutgers University, New Jersey, USA, 1996.","DOI":"10.7146\/brics.v3i24.20005"},{"key":"10.1016\/j.jlap.2005.05.001_bib29","series-title":"The C Programming Language","author":"Kernighan","year":"1988"},{"issue":"1\u20132","key":"10.1016\/j.jlap.2005.05.001_bib30","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"Uppaal in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"Int. J. Software Tools Technol. Transfer"},{"key":"10.1016\/j.jlap.2005.05.001_bib31","series-title":"in: Proceedings of the 18th IEEE Real-Time Systems Symposium","first-page":"14","article-title":"Efficient verification of real-time systems: compact data structures and state-space reduction","author":"Larsson","year":"1997"},{"key":"10.1016\/j.jlap.2005.05.001_bib32","first-page":"353","article-title":"Formal design and analysis of a gear controller","volume":"3","author":"Lindahl","year":"2001","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/j.jlap.2005.05.001_bib33","series-title":"Specification of Abstract Data Types","author":"Loeckx","year":"1996"},{"key":"10.1016\/j.jlap.2005.05.001_bib34","unstructured":"B. Luttik, Choice quantification in process algebra, Ph.D. thesis, University of Amsterdam, 2002."},{"issue":"3","key":"10.1016\/j.jlap.2005.05.001_bib35","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","article-title":"Efficient on-the-fly model-checking for regular alternation-free mu-calculus","volume":"46","author":"Mateescu","year":"2003","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlap.2005.05.001_bib36","unstructured":"M.O. M\u00f6ller, Structure and hierarchy in real-time systems, Ph.D. thesis, University of Aarhus, 2002."},{"issue":"2","key":"10.1016\/j.jlap.2005.05.001_bib37","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","article-title":"Three logics for branching bisimulation","volume":"42","author":"De Nicola","year":"1995","journal-title":"J. ACM"},{"key":"10.1016\/j.jlap.2005.05.001_bib38","doi-asserted-by":"crossref","unstructured":"S. Owre, J.M. Rushby, N. Shankar, PVS: a Prototype Verification System, in: Proceedings of the 11th Conference on Automated Deduction (CADE\u201992), Lecture Notes in Computer Science, vol. 607, 1992, pp. 748\u2013752.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"10.1016\/j.jlap.2005.05.001_bib39","unstructured":"N. Tr\u010dka, Verifying \u03c7 Models of Industrial Systems with Spin, CS-Report 05-12, Eindhoven University of Technology, 2005."},{"issue":"1","key":"10.1016\/j.jlap.2005.05.001_bib40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0167-6423(01)00018-1","article-title":"State space generation for the HAVi leader election protocol","volume":"43","author":"Usenko","year":"2002","journal-title":"Sci. Comput. Program"},{"key":"10.1016\/j.jlap.2005.05.001_bib41","unstructured":"TIPSy Project Website. Available from: ."},{"key":"10.1016\/j.jlap.2005.05.001_bib42","series-title":"Proceedings of the 10th Conference on Engineering of Complex Computer Systems (ICECCS\u201905)","first-page":"184","article-title":"From \u03c7t to \u03bcCRL: combining performance and functional analysis","author":"Wijs","year":"2005"}],"container-title":["The Journal of Logic and Algebraic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832605000524?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1567832605000524?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T19:59:29Z","timestamp":1586375969000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1567832605000524"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,11]]}},"alternative-id":["S1567832605000524"],"URL":"https:\/\/doi.org\/10.1016\/j.jlap.2005.05.001","relation":{},"ISSN":["1567-8326"],"issn-type":[{"value":"1567-8326","type":"print"}],"subject":[],"published":{"date-parts":[[2005,11]]}}}