{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T06:16:33Z","timestamp":1770790593099,"version":"3.50.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Software Engineering"],"published-print":{"date-parts":[[1997,1]]},"DOI":"10.1023\/a:1018965316985","type":"journal-article","created":{"date-parts":[[2003,2,19]],"date-time":"2003-02-19T22:07:13Z","timestamp":1045692433000},"page":"189-219","source":"Crossref","is-referenced-by-count":7,"title":["Engineering formal requirements: An analysis and testing method for Z documents"],"prefix":"10.1007","volume":"3","author":[{"given":"P.","family":"Ciancarini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Cimato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Mascolo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"326126_CR1","volume-title":"Z in Practice","author":"R. Barden","year":"1994","unstructured":"Barden, R., S. Stepney, and D. Cooper (1994), Z in Practice, Prentice-Hall, London."},{"key":"326126_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-60692-0_41","volume-title":"Proc. 15th Conference on Foundation of Software Technology and Theoretical Computer Science, Bangalore, India","author":"P. Baumann","year":"1995","unstructured":"Baumann, P. and K. Lermer (1995), \u201cA Framework for the Specification of Reactive and Concurrent Systems in Z,\u201d In Proc. 15th Conference on Foundation of Software Technology and Theoretical Computer Science, Bangalore, India, P. Thiagarajan, Ed., Lecture Notes in Computer Science, vol. 1026, Springer-Verlag, Berlin, pp. 62\u201379."},{"key":"326126_CR3","first-page":"221","volume-title":"Proc. 4th Z Users Workshop (ZUM89), Oxford","author":"M. Benjamin","year":"1989","unstructured":"Benjamin, M. (1989), \u201cA Message Passing System. An example of combining Z and CSP,\u201d In Proc. 4th Z Users Workshop (ZUM89), Oxford, J. Nicholls, Ed., Workshops in Computing, Springer-Verlag, Berlin, pp. 221\u2013228."},{"key":"326126_CR4","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G. Berry","year":"1992","unstructured":"Berry, G. and G. Boudol (1992), \u201cThe Chemical Abstract Machine,\u201d Theoretical Computer Science 96, 217\u2013248.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"326126_CR5","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1142\/S0218194095000290","volume":"5","author":"A. Bloesch","year":"1995","unstructured":"Bloesch, A., E. Kazmierczak, P. Kearney, and O. Traynor, (1995), \u201cCogito: Methodology and System for Formal Software Development,\u201d Int. Journal on Software Engineering and Knowledge Engineering 5,4, 599\u2013618.","journal-title":"Int. Journal on Software Engineering and Knowledge Engineering"},{"key":"326126_CR6","series-title":"Lecture Notes in Computer Science","first-page":"92","volume-title":"A Decade of Concurrency","author":"G. Boudol","year":"1993","unstructured":"Boudol, G. (1993), \u201cSome Chemical Abstract Machines,\u201d In A Decade of Concurrency, J. de Bakker, W. de Roever, and G. Rozenberg, Eds., Lecture Notes in Computer Science, Vol. 803, Springer-Verlag, Berlin, pp. 92\u2013123."},{"key":"326126_CR7","first-page":"141","volume-title":"Proc. 8th Z Users Workshop (ZUM94)","author":"J. Bowen","year":"1994","unstructured":"Bowen, J. and M. Gordon (1994), \u201cZ and HOL,\u201d In Proc. 8th Z Users Workshop (ZUM94), Cambridge, J. Bowen and J. Hall, Eds., Workshops in Computing, Springer-Verlag, Berlin, pp. 141\u2013167."},{"issue":"5\u20136","key":"326126_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J. Bowen","year":"1995","unstructured":"Bowen, J. and M. Gordon (1995), \u201cA Shallow Embedding of Z in HOL,\u201d Information and Software Technology 37,5\u20136, 269\u2013276.","journal-title":"Information and Software Technology"},{"key":"326126_CR9","first-page":"185","volume-title":"Proc. 8th Z Users Workshop (ZUM94)","author":"P. Breuer","year":"1994","unstructured":"Breuer, P. and J. Bowen (1994), \u201cTowards Correct Executable Semantics for Z,\u201d In Proc. 8th Z Users Workshop (ZUM94), Cambridge, J. Bowen and J. Hall, Eds., Workshops in Computing, Springer-Verlag, Berlin, pp. 185\u2013212."},{"key":"326126_CR10","unstructured":"Brien, S. and J. Nicholls (1992), \u201cZ Base Standard, November 1992,\u201d Programming Research Group."},{"key":"326126_CR11","first-page":"281","volume-title":"Formal Description Techniques (FORTE 89)","author":"D. Carrington","year":"1989","unstructured":"Carrington, D., D. Duke, R. Duke, P. King, G. Rose, and G. Smith (1989), \u201cObject-Z: an Object-Oriented Extension to Z,\u201d In Formal Description Techniques (FORTE 89), North-Holland, Amsterdam, pp. 281\u2013296."},{"key":"326126_CR12","volume-title":"Parallel Programming Design","author":"K. M. Chandy","year":"1988","unstructured":"Chandy, K. M. and J. Misra (1988), Parallel Programming Design, Addison-Wesley, Reading, MA."},{"key":"326126_CR13","doi-asserted-by":"crossref","unstructured":"Ciaccia, P., P. Ciancarini, and W. Penzo (1996), \u201cA Formal Approach to Software Design: The Clepsydra Methodology,\u201d Int. Journal on Software Engineering and Knowledge Engineering. To appear.","DOI":"10.1007\/3-540-60271-2_110"},{"key":"326126_CR14","series-title":"Lecture Notes in Computer Science","first-page":"110","volume-title":"Research Directions in High-Level Parallel Programming Languages","author":"P. Ciancarini","year":"1991","unstructured":"Ciancarini, P. (1991), \u201cParallel Logic Programming Using the Linda Model of Computation,\u201d In Research Directions in High-Level Parallel Programming Languages, Mont Saint-Michel, France, J. Banatre and D. LeMetayer, Eds., Lecture Notes in Computer Science, Vol. 574, Springer-Verlag, Berlin, pp. 110\u2013125."},{"key":"326126_CR15","doi-asserted-by":"crossref","unstructured":"Ciancarini, P. and M. Gaspari (1996), \u201cRule Based Coordination of Logic Programs,\u201d Computer Languages. To appear.","DOI":"10.1016\/S0096-0551(96)00009-4"},{"key":"326126_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"639","DOI":"10.1007\/3-540-58555-9_120","volume-title":"FME'94: Industrial Benefit of Formal Methods","author":"J. Cuellar","year":"1994","unstructured":"Cuellar, J., I. Wildgruber, and D. Barnard (1994), \u201cCombining the Design of Industrial Systems with Effective Verification Techniques,\u201d In FME'94: Industrial Benefit of Formal Methods, Barcelona, Spain, Lecture Notes in Computer Science, Vol. 873, Springer-Verlag, Berlin, pp. 639\u2013658."},{"key":"326126_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/3-540-61042-1_39","volume-title":"Proc. TACAS '96","author":"C. Damon","year":"1996","unstructured":"Damon, C. and D. Jackson (1996), \u201cEfficient Search as a Means of Executing Specifications,\u201d In Proc. TACAS '96, T. Margaria and B. Steffen, Eds., Lecture Notes in Computer Science, Vol. 1055, Springer-Verlag, Berlin, pp. 70\u201386."},{"key":"326126_CR18","first-page":"71","volume-title":"Proc. 4th Z Users Workshop","author":"A. Dick","year":"1989","unstructured":"Dick, A., P. Krause, and J. Cozens (1989), \u201cComputer Aided Transformation of Z into Prolog,\u201d In Proc. 4th Z Users Workshop, J. Nicholls Ed., Workshops in Computing, Springer-Verlag, Berlin, pp. 71\u201385."},{"key":"326126_CR19","unstructured":"Diller, A. (1990), Z: An Introduction to Formal Methods, Wiley."},{"key":"326126_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-54834-3_13","volume-title":"VDM 91: Formal Software Development Methods","author":"V. Doma","year":"1991","unstructured":"Doma, V. and R. Nicholl (1991), \u201cEZ: A System for Automatic Prototyping of Z Specifications,\u201d In VDM 91: Formal Software Development Methods, Noordwijkerhout, S. Prehn and W. Toetenel, Eds., Lecture Notes in Computer Science, Vol. 551, Springer-Verlag, Berlin, pp. 189\u2013203."},{"key":"326126_CR21","first-page":"269","volume-title":"Proc. 8th Z Users Workshop (ZUM94)","author":"A. Evans","year":"1994","unstructured":"Evans, A. (1994a), \u201cVisualizing Concurrent Z Specifications,\u201d In Proc. 8th Z Users Workshop (ZUM94), Cambridge, J. Bowen and J. Hall, Eds., Workshops in Computing, Springer-Verlag, Berlin, pp. 269\u2013281."},{"key":"326126_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/3-540-58555-9_105","volume-title":"Proc. FME'94 Industrial Benefits of Formal Methods","author":"A. Evans","year":"1994","unstructured":"Evans, A. (1994b), \u201cSpecifying and Verifying Concurrent Systems Using Z,\u201d In Proc. FME'94 Industrial Benefits of Formal Methods, M. Bertran, T. Denvir, and M. Naftalin, Eds., Lecture Notes in Computer Science, Vol. 873, Springer-Verlag, Berlin, pp. 366\u2013380."},{"issue":"5","key":"326126_CR23","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1049\/sej.1992.0033","volume":"7","author":"N. Fuchs","year":"1992","unstructured":"Fuchs, N. (1992), \u201cSpecifications are (Preferably) Executable,\u201d IEE Software Engineering Journal 7,5, 323\u2013334.","journal-title":"IEE Software Engineering Journal"},{"key":"326126_CR24","first-page":"3","volume-title":"Proc. 5th Z Users Workshop","author":"P. Gardiner","year":"1990","unstructured":"Gardiner, P., P. Lupton, and J. Woodcock (1990), \u201cA Simpler Semantics for Z,\u201d In Proc. 5th Z Users Workshop, Oxford, J. Nicholls, Ed., Workshops in Computing, Springer-Verlag, Berlin, pp. 3\u201311."},{"key":"326126_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/BFb0022111","volume-title":"Proc. 1st European Software Eng. Conf. (ESEC 87)","author":"F. Garzotto","year":"1987","unstructured":"Garzotto, F., C. Ghezzi, D. Mandrioli, and A. Morzenti (1987), \u201cOn the Specification of Real-Time Systems Using Logic Programming,\u201d In Proc. 1st European Software Eng. Conf. (ESEC 87), Lecture Notes in Computer Science, Vol. 289, Springer-Verlag, Berlin, pp. 180\u2013190."},{"key":"326126_CR26","unstructured":"Hayes, I. (1993), Specification Case Studies, Prentice-Hall, 2nd edition."},{"issue":"6","key":"326126_CR27","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1049\/sej.1989.0045","volume":"4","author":"I. Hayes","year":"1989","unstructured":"Hayes, I. and C. Jones (1989), \u201cSpecifications are not (Necessarily) Executable,\u201d IEE Software Engineering Journal 4,6, 330\u2013338.","journal-title":"IEE Software Engineering Journal"},{"key":"326126_CR28","first-page":"173","volume-title":"Proc. 7th Int. Conf. on Software Engineering and Knowledge Engineering","author":"X. He","year":"1995","unstructured":"He, X. (1995), \u201cPZ Nets: A Formal Method Integrating Petri Nets with Z,\u201d In Proc. 7th Int. Conf. on Software Engineering and Knowledge Engineering, Rockville, Maryland, Knowledge Systems Institute, pp. 173\u2013180."},{"issue":"4","key":"326126_CR29","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1109\/32.385973","volume":"21","author":"P. Inverardi","year":"1995","unstructured":"Inverardi, P. and A. Wolf (1995), \u201cFormal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model,\u201d IEEE Transactions on Software Engineering 21,4, 373\u2013386.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"326126_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/3-540-58555-9_113","volume-title":"Proc. 2nd Int. Symp. of Formal Methods Europe (FME)","author":"D. Jackson","year":"1994","unstructured":"Jackson, D. (1994), \u201cAbstract Model Checking of Infinite Specifications,\u201d In Proc. 2nd Int. Symp. of Formal Methods Europe (FME), Barcelone, Spain, M. Naftalin, T. Denvir, and M. Bertran, Eds., Lecture Notes in Computer Science, Vol. 873, Springer-Verlag, Berlin, pp. 519\u2013531."},{"key":"326126_CR31","unstructured":"Jia, X. (1994), \u201cZTC: A Type Checker for Z,\u201d User's Guide, 1994. Institute of Software Engineering."},{"issue":"1","key":"326126_CR32","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/TSE.1985.231535","volume":"11","author":"R. Kemmerer","year":"1985","unstructured":"Kemmerer, R. (1985), \u201cTesting Formal Specifications to Detect Design Errors,\u201d IEEE Transactions on Software Engineering 11,1, 32\u201343.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"326126_CR33","unstructured":"Knott, R. and P. Krause (1992), In The Unified Computation Laboratory, Oxford, C. Rattray and R. Clark, Eds., IMA Conference Series, Vol. 35, Clarendon Press, pp. 207\u2013220."},{"key":"326126_CR34","first-page":"267","volume-title":"Proc. 8th Z Users Workshop (ZUM94)","author":"L. Lamport","year":"1994","unstructured":"Lamport, L. (1994), In Proc. 8th Z Users Workshop (ZUM94), Cambridge, J. Bowen and J. Hall, Eds., Workshops in Computing, Springer-Verlag, Berlin, pp. 267\u2013268."},{"key":"326126_CR35","doi-asserted-by":"crossref","unstructured":"Richardson, D., S. Aha, and T. O'Malley (1992), \u201cSpecification-based Test Oracles for Reactive Systems,\u201d In Proc. 14th IEEE Int. Conf. on Software Engineering, Melbourne, Australia, pp. 105\u2013118.","DOI":"10.1145\/143062.143100"},{"key":"326126_CR36","first-page":"223","volume-title":"Proc. Z User Workshop","author":"M. Saaltnik","year":"1989","unstructured":"Saaltnik, M. (1989), \u201cZ and Eves,\u201d In Proc. Z User Workshop, Oxford, UK, J. Nicholls, Ed., Workshops in Computing, Springer-Verlag, Berlin, pp. 223\u2013242."},{"key":"326126_CR37","unstructured":"Spivey, J. (1988a), Understanding Z, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press."},{"key":"326126_CR38","unstructured":"Spivey, J. (1988b), The f\n                  Uzz\n                  Manual."},{"key":"326126_CR39","unstructured":"Spivey, J. (1992), The Z Notation, A Reference Manual, Prentice-Hall, 2nd edition."},{"issue":"1","key":"326126_CR40","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1142\/S0218194096000041","volume":"6","author":"L. Sterling","year":"1996","unstructured":"Sterling, L., P. Ciancarini, and T. Turnidge (1996), \u201cOn the Animation of Not Executable Specifications by Prolog,\u201d Int. Journal on Software Engineering and Knowledge Engineering 6,1, 63\u201388.","journal-title":"Int. Journal on Software Engineering and Knowledge Engineering"},{"issue":"5\u20136","key":"326126_CR41","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/0950-5849(95)99365-T","volume":"37","author":"S. Valentine","year":"1995","unstructured":"Valentine, S. (1995), \u201cThe Programming Language Z-,\u201d Information and Software Technology 37,5\u20136, 293\u2013302.","journal-title":"Information and Software Technology"},{"key":"326126_CR42","series-title":"Lecture Notes in Computer Sciences","first-page":"204","volume-title":"Proc. VDM 91: Formal Software Development Methods","author":"K. van Hee","year":"1991","unstructured":"van Hee, K., L. Somers, and Voorhoeve (1991), \u201cZ and High Level Petri Nets,\u201d In Proc. VDM 91: Formal Software Development Methods, S. Prehn and W. Toetenel, Eds., Lecture Notes in Computer Sciences, Vol. 551, Springer-Verlag, Berlin, pp. 204\u2013219."},{"key":"326126_CR43","unstructured":"Wordsworth, J. (1992), Software Development with Z, Addison-Wesley."}],"container-title":["Annals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018965316985.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1018965316985\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1018965316985.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T14:17:09Z","timestamp":1747577829000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1018965316985"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,1]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1997,1]]}},"alternative-id":["326126"],"URL":"https:\/\/doi.org\/10.1023\/a:1018965316985","relation":{},"ISSN":["1022-7091","1573-7489"],"issn-type":[{"value":"1022-7091","type":"print"},{"value":"1573-7489","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997,1]]}}}