{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:11:42Z","timestamp":1761610302477,"version":"build-2065373602"},"reference-count":22,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,10,1]],"date-time":"2003-10-01T00:00:00Z","timestamp":1064966400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3589,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,10]]},"DOI":"10.1016\/s1571-0661(04)81040-5","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"2-21","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":15,"title":["Runtime Conformance Checking of Objects Using Alloy"],"prefix":"10.1016","volume":"89","author":[{"given":"Michelle L.","family":"Crane","sequence":"first","affiliation":[]},{"given":"Juergen","family":"Dingel","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB1","unstructured":"Bhorkar A., A run-time assertion checker for Java using JML, Technical report, Department of Computer Science, Iowa State University (2000)."},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB2","unstructured":"Biagioni E., R. Harper and P. Lee, Implementing software architectures in Standard ML, Position Paper (1994)."},{"year":"1999","series-title":"\u201cThe Unified Modeling Language User Guide,\u201d","author":"Booch","key":"10.1016\/S1571-0661(04)81040-5_NEWBIB3"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB4","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: State of the art and future directions","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB5","unstructured":"Crane, M. L. and J. Dingel, Embee performance results, Technical Report 2003\u2013465, School of Computing, Queen's University (2003). URL http:\/\/www.cs.queensu.ca\/TechReports\/Reports\/2003-465.pdf"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB6","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/S1571-0661(04)00253-1","article-title":"Monitoring Java programs with Java PathExplorer","volume":"55","author":"Havelund","year":"2001","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Jackson D., Automating first-order relational logic, in: Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering (2000), pp. 130\u2013139.","DOI":"10.1145\/355045.355063"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Jackson D., Enforcing design constraints with object logic, in: Static Analysis Symposium, 2000, pp. 1\u201321.","DOI":"10.1007\/978-3-540-45099-3_1"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB9","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","article-title":"Alloy: A lightweight object modelling notation","volume":"11","author":"Jackson","year":"2002","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB10","unstructured":"Jackson D., Micromodels of software: Lightweight modelling and analysis with Alloy, Technical report, Software Design Group, MIT Lab for Computer Science (2002)."},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB11","doi-asserted-by":"crossref","unstructured":"Jackson D., I. Schechter and I. Shlyakhter, Alcoa: The Alloy constraint analyzer, in: Proceedings of the 22nd International Conference on Software Engineering (2000), pp. 730\u2013733.","DOI":"10.1145\/337180.337616"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB12","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(04)00254-3","article-title":"Java-MaC: A run-time assurance tool for Java programs","volume":"55","author":"Kim","year":"2001","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB13","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","article-title":"JML: A notation for detailed design","author":"Leavens","year":"1999","journal-title":"Behavioral Specifications of Businesses and Systems"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB14","series-title":"OOPSLA 2000 Companion","first-page":"105","article-title":"JML: Notations and tools supporting detailed design in Java","author":"Leavens","year":"2000"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB15","unstructured":"Lee I., S. Kannan, M. Kim, O. Sokolsky and M. Viswanathan, Runtime assurance based on formal specifications, in: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999."},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB16","unstructured":"Marinov D. and S. Khurshid, TestEra: A novel framework for automated testing of Java programs, in: 16th IEEE International Conference on Automated Software Engineering (ASE'01), 2001, pp. 22\u201332."},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB17","unstructured":"Microsystems S., JavaTM Platform Debugger Architecture. URL http:\/\/java.sun.com\/products\/jpda"},{"year":"1992","series-title":"\u201cThe Z Notation: A Reference Manual,\u201d","author":"Spivey","key":"10.1016\/S1571-0661(04)81040-5_NEWBIB18"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB19","unstructured":"Turner C., T. Graham, H. Stewart, C. Wolfe and A. Ryman, Visual constraint diagrams: Runtime conformance checking of UML object models versus implementations (2002), unpublished manuscript."},{"year":"1999","series-title":"\u201cThe Object Constraint Language: Precise Modeling with UML,\u201d","author":"Warmer","key":"10.1016\/S1571-0661(04)81040-5_NEWBIB20"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB21","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/268999.269003","article-title":"Software reliability via run-time result-checking","volume":"44","author":"Wasserman","year":"1997","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(04)81040-5_NEWBIB22","series-title":"A specifier's introduction to formal methods, Computer","first-page":"8","author":"Wing","year":"1990"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810405?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810405?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:48Z","timestamp":1761610008000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104810405"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,10]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,10]]}},"alternative-id":["S1571066104810405"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)81040-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2003,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Runtime Conformance Checking of Objects Using Alloy","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)81040-5","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}