乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,3,18]],"date-time":"2023-03-18T23:26:03Z","timestamp":1679181963532},"reference-count":55,"publisher":"Elsevier BV","issue":"10","license":[{"start":{"date-parts":[[2009,8,1]],"date-time":"2009-08-01T00:00:00Z","timestamp":1249084800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,10,3]],"date-time":"2013-10-03T00:00:00Z","timestamp":1380758400000},"content-version":"vor","delay-in-days":1524,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2009,8]]},"DOI":"10.1016\/j.scico.2009.03.003","type":"journal-article","created":{"date-parts":[[2009,3,30]],"date-time":"2009-03-30T21:41:31Z","timestamp":1238449291000},"page":"812-835","source":"Crossref","is-referenced-by-count":6,"title":["Invariant-driven specifications in Maude"],"prefix":"10.1016","volume":"74","author":[{"given":"Manuel","family":"Rold\u00e1n","sequence":"first","affiliation":[]},{"given":"Francisco","family":"Dur\u00e1n","sequence":"additional","affiliation":[]},{"given":"Antonio","family":"Vallecillo","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2009.03.003_b1","series-title":"The B Book \u2014 Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"10.1016\/j.scico.2009.03.003_b2","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","article-title":"The KeY tool","volume":"4","author":"Ahrendt","year":"2005","journal-title":"Software and System Modeling"},{"key":"10.1016\/j.scico.2009.03.003_b3","series-title":"Fifth Annual Symposium on Logic in Computer Science","first-page":"390","article-title":"Real time logics: Complexity and expressiveness","author":"Alur","year":"1990"},{"key":"10.1016\/j.scico.2009.03.003_b4","series-title":"Verification of Object-Oriented Software: The KeY Approach","volume":"vol. 4334","year":"2007"},{"key":"10.1016\/j.scico.2009.03.003_b5","unstructured":"P. Borovansk\u00fd, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, C. Ringeissen, M. Vittek, ELAN v 3.3 user manual, third edition. Technical Report, INRIA Lorraine & LORIA, Nancy, France, December 1998"},{"issue":"2","key":"10.1016\/j.scico.2009.03.003_b6","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0304-3975(01)00358-9","article-title":"ELAN from the rewriting logic point of view","volume":"285","author":"Borovansk\u00fd","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.scico.2009.03.003_b7","series-title":"Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of ETAPS 2002, Grenoble, France, April 2002, Proceedings","first-page":"203","article-title":"Enriching OCL using observational mu-calculus","volume":"vol. 2306","author":"Bradfield","year":"2002"},{"key":"10.1016\/j.scico.2009.03.003_b8","doi-asserted-by":"crossref","unstructured":"M. Bravenboer, K.T. Kalleberg, R. Vermaas, E. Visser, Stratego\/XT tutorial, examples, and reference manual, Department of Information and Computing Sciences, Universiteit Utrecht., Utrecht, The Netherlands, 2006","DOI":"10.1145\/1111542.1111558"},{"key":"10.1016\/j.scico.2009.03.003_b9","series-title":"Model Checking","author":"Clarke","year":"1999"},{"issue":"3","key":"10.1016\/j.scico.2009.03.003_b10","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/1127878.1127900","article-title":"A historical perspective on runtime assertion checking in software development","volume":"31","author":"Clarke","year":"2006","journal-title":"SIGSOFT Software Engineering Notes"},{"issue":"3","key":"10.1016\/j.scico.2009.03.003_b11","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/1127878.1127900","article-title":"A historical perspective on runtime assertion checking in software development","volume":"31","author":"Clarke","year":"2006","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"10.1016\/j.scico.2009.03.003_b12","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","article-title":"Maude: Specification and programming in rewriting logic","volume":"285","author":"Clavel","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.scico.2009.03.003_b13","series-title":"All About Maude \u2014 A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic","author":"Clavel","year":"2007"},{"key":"10.1016\/j.scico.2009.03.003_b14","unstructured":"M. Clavel, F. Dur\u00e1n, S. Eker, P. Lincoln, N. Mart\u00ed-Oliet, J. Meseguer, C. Talcott, Maude 2.4 manual, November 2008. Available in: http:\/\/maude.cs.uiuc.edu"},{"key":"10.1016\/j.scico.2009.03.003_b15","series-title":"FM\u201999 \u2014 Formal Methods (Vol. II)","first-page":"1684","article-title":"Maude as a formal meta-tool","volume":"vol. 1709","author":"Clavel","year":"1999"},{"key":"10.1016\/j.scico.2009.03.003_b16","series-title":"Unified Modeling Language: Systems Analysis, Design, and Development Issues","first-page":"151","article-title":"Temporal OCL: Meeting specification demands for business components","author":"Conrad","year":"2001"},{"key":"10.1016\/j.scico.2009.03.003_b17","series-title":"Abstract State Machines, B and Z. Abstract State Machines, B and Z First International Conference, ABZ 2008, London, UK, September 16\u201318, 2008, Proceedings","first-page":"280","article-title":"Z2SAL \u2014 building a model checker for Z","volume":"vol. 5238","author":"Derrick","year":"2008"},{"key":"10.1016\/j.scico.2009.03.003_b18","series-title":"Algebraic Methodology and Software Technology","first-page":"117","article-title":"Linear temporal logic and Z refinement","volume":"vol. 3116","author":"Derrick","year":"2004"},{"key":"10.1016\/j.scico.2009.03.003_b19","series-title":"Formal Methods for Open Object-based Distributed Systems, FMOODS 2000, IFIP Conference Proceedings","first-page":"305","article-title":"On a temporal logic for object-based systems","author":"Distefano","year":"2000"},{"key":"10.1016\/j.scico.2009.03.003_b20","series-title":"Proceedings of Fifth International Workshop on Rule-Based Programming","first-page":"25","article-title":"On-demand evaluation for Maude","volume":"vol. 124","author":"Dur\u00e1n","year":"2004"},{"key":"10.1016\/j.scico.2009.03.003_b21","series-title":"5th International Workshop on Rewriting Logic and its Applications","first-page":"263","article-title":"New evaluation commands for Maude within Full Maude","volume":"vol. 117","author":"Dur\u00e1n","year":"2005"},{"key":"10.1016\/j.scico.2009.03.003_b22","series-title":"Proceedings Second International Workshop on Rewriting Logic and its Applications","first-page":"185","article-title":"An extensible module algebra for Maude","volume":"vol. 15","author":"Dur\u00e1n","year":"1998"},{"key":"10.1016\/j.scico.2009.03.003_b23","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1016\/S0304-3975(03)00312-8","article-title":"Structured theories and institutions","volume":"309","author":"Dur\u00e1n","year":"2003","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/j.scico.2009.03.003_b24","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.scico.2006.07.002","article-title":"Maude\u2019s module algebra","volume":"66","author":"Dur\u00e1n","year":"2007","journal-title":"Science of Computer Programming"},{"key":"10.1016\/j.scico.2009.03.003_b25","unstructured":"F. Dur\u00e1n, M. Rold\u00e1n, The price of going to the metalevel: Invariant driven execution, Technical Report, Departamento de Lenguajes y Ciencias de la Computaci\u00f3n, Universidad de M\u00e1laga, 2007"},{"issue":"6","key":"10.1016\/j.scico.2009.03.003_b26","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1016\/j.csi.2004.10.008","article-title":"Using Maude to write and execute ODP information viewpoint specifications","volume":"27","author":"Dur\u00e1n","year":"2005","journal-title":"Computer Standards and Interfaces"},{"key":"10.1016\/j.scico.2009.03.003_b27","series-title":"Proceedings of 4th International Workshop on Rewriting Logic and its Applications","article-title":"The Maude LTL model checker","author":"Eker","year":"2002"},{"key":"10.1016\/j.scico.2009.03.003_b28","series-title":"Modelling Systems: Practical Tools and Techniques in Software Development","author":"Fitzgerald","year":"1998"},{"key":"10.1016\/j.scico.2009.03.003_b29","series-title":"UML 2002 \u2014 The Unified Modeling Language, 5th International Conference, Dresden, Germany, September 30\u2013October 4, 2002, Proceedings","first-page":"179","article-title":"A UML profile for real-time constraints with the OCL","volume":"vol. 2460","author":"Flake","year":"2002"},{"key":"10.1016\/j.scico.2009.03.003_b30","series-title":"Software Engineering with OBJ: Algebraic Specification in Action","article-title":"Introducing OBJ","author":"Goguen","year":"2000"},{"key":"10.1016\/j.scico.2009.03.003_b31","series-title":"Proceedings of Automated Software Engineering 2001","first-page":"135","article-title":"Monitoring programs using rewriting","author":"Havelund","year":"2001"},{"key":"10.1016\/j.scico.2009.03.003_b32","series-title":"Proceedings of the 1st Workshop on Runtime Verification","volume":"vol. 55","year":"2001"},{"issue":"2","key":"10.1016\/j.scico.2009.03.003_b33","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","article-title":"Rewriting-based techniques for runtime verification","volume":"12","author":"Havelund","year":"2005","journal-title":"Journal of Automated Software Engineering"},{"key":"10.1016\/j.scico.2009.03.003_b34","series-title":"Proceedings of 10th International Conference of Z Users","first-page":"37","article-title":"Experiences with PiZA, an animator for Z","volume":"vol. 1212","author":"Hewitt","year":"1997"},{"key":"10.1016\/j.scico.2009.03.003_b35","series-title":"The SPIN Model Checker","author":"Holzmann","year":"2003"},{"key":"10.1016\/j.scico.2009.03.003_b36","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/0004-3702(85)90074-8","article-title":"Refutational theorem proving using term rewriting systems","volume":"25","author":"Hsiang","year":"1985","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.scico.2009.03.003_b37","unstructured":"X. Jia, A tutorial of ZANS, DePaul University, Chicago, Illinois, USA, 0.3 edition, October 2002"},{"key":"10.1016\/j.scico.2009.03.003_b38","series-title":"Systematic Software Development using VDM","author":"Jones","year":"1990"},{"key":"10.1016\/j.scico.2009.03.003_b39","series-title":"Specification in B: An Introduction using the B-Toolkit","author":"Lano","year":"1996"},{"key":"10.1016\/j.scico.2009.03.003_b40","first-page":"1","article-title":"Rewriting logic as a logical and semantic framework","volume":"vol. 9","author":"Mart\u00ed-Oliet","year":"2002"},{"key":"10.1016\/j.scico.2009.03.003_b41","series-title":"4th International Workshop on Rewriting Logic and its Applications","first-page":"417","article-title":"Towards a strategy language for Maude","volume":"vol. 117","author":"Mart\u00ed-Oliet","year":"2005"},{"key":"10.1016\/j.scico.2009.03.003_b42","doi-asserted-by":"crossref","unstructured":"T. McComb, G. Smith, Animation of object-Z specifications using a Z animator, in: First International Conference on Software Engineering and Formal Methods, SEFM\u201903, 2003","DOI":"10.1109\/SEFM.2003.1236221"},{"key":"10.1016\/j.scico.2009.03.003_b43","series-title":"Executable UML: A Foundation for Model-Driven Architecture","author":"Mellor","year":"2002"},{"issue":"1","key":"10.1016\/j.scico.2009.03.003_b44","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.scico.2009.03.003_b45","series-title":"Recent Trends in Algebraic Development Techniques","first-page":"18","article-title":"Membership algebra as a logical framework for equational specification","volume":"vol. 1376","author":"Meseguer","year":"1998"},{"key":"10.1016\/j.scico.2009.03.003_b46","unstructured":"OMG, Object constraint language (OMG OCL), v2.0. OMG Available Specification (formal\/2006-05-01), 2006"},{"key":"10.1016\/j.scico.2009.03.003_b47","unstructured":"OMG, Unified modeling language (OMG UML), v2.1.2. OMG Available Specification (formal\/2007-11-04), 2007"},{"key":"10.1016\/j.scico.2009.03.003_b48","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, 1977, pp. 46\u201377","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/j.scico.2009.03.003_b49","unstructured":"S. Ramakrishnan, J. McGregor, Extending OCL to support temporal operators, in: A. Ulrich, G. Chrobok-Diening (Eds.), Proceedings of the Workshop on Testing Distributed Component-Based Systems, 1999"},{"key":"10.1016\/j.scico.2009.03.003_b50","series-title":"Advances in Object Modelling with the OCL","first-page":"43","article-title":"OCL: Syntax, semantics and tools","volume":"vol. 2263","author":"Richters","year":"2001"},{"key":"10.1016\/j.scico.2009.03.003_b51","series-title":"The Z Notation","author":"Spivey","year":"1992"},{"key":"10.1016\/j.scico.2009.03.003_b52","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/j.entcs.2004.01.029","article-title":"Monitoring algorithms for metric temporal logic specifications","volume":"113","author":"Thati","year":"2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/j.scico.2009.03.003_b53","unstructured":"M. Utting, Jaza user manual and tutorial, The University of Waikato, Hamilton, New Zealand, June 2005"},{"key":"10.1016\/j.scico.2009.03.003_b54","series-title":"Rewriting Techniques and Applications","first-page":"357","article-title":"Stratego: A language for program transformation based on rewriting strategies. System description of stratego 0.5","volume":"vol. 2051","author":"Visser","year":"2001"},{"key":"10.1016\/j.scico.2009.03.003_b55","series-title":"5th Int. Conf. Perspectives of System Informatics","article-title":"OCL extended with temporal logic","volume":"vol. 2890","author":"Ziemann","year":"2003"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642309000501?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642309000501?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T05:40:24Z","timestamp":1558244424000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642309000501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8]]},"references-count":55,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2009,8]]}},"alternative-id":["S0167642309000501"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2009.03.003","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2009,8]]}}}