{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:50Z","timestamp":1725484610440},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431664"},{"type":"electronic","value":"9783540456483"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_3","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T05:26:02Z","timestamp":1180329962000},"page":"42-61","source":"Crossref","is-referenced-by-count":5,"title":["Controlling Control Systems: An Application of Evolving Retrenchment"],"prefix":"10.1007","author":[{"given":"Michael","family":"Poppleton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Banach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"3_CR1","unstructured":"K.E. Atkinson. An Introduction to Numerical Analysis. Wiley, 1989."},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"R. J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1007\/s002360050148","volume":"35","author":"R.J.R. Back","year":"1998","unstructured":"R.J.R. Back and M. Butler. Fusion and simultaneous execution in the refinement calculus. Acta Informatica, 35:921\u2013949, 1998.","journal-title":"Acta Informatica"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"R. Banach. Maximally abstract retrenchments. In Proc. IEEE ICFEM2000, pages 133\u2013142, York, August 2000. IEEE Computer Society Press.","DOI":"10.1109\/ICFEM.2000.873813"},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BFb0053358","volume-title":"Retrenchment: An engineering variation on refinement","author":"R. Banach","year":"1998","unstructured":"R. Banach and M. Poppleton. Retrenchment: An engineering variation on refinement. In D. Bert, editor, 2nd International B Conference, volume 1393 of LNCS, pages 129\u2013147, Montpellier, France, April 1998. Springer."},{"key":"3_CR6","unstructured":"R. Banach and M. Poppleton. Retrenchment: An engineering variation on refinement. Technical Report Report UMCS-99-3-2, University of Manchester Computer Science Department, 1999."},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"R. Banach and M. Poppleton. Retrenchment and punctured simulation. In K. Araki, A. Galloway, and K. Taguchi, editors, Proc. IFM\u201999:Integrated Formal Methods 1999, pages 457\u2013476, University of York, June 1999. Springer.","DOI":"10.1007\/978-1-4471-0851-1_24"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/s001650050056","volume":"11","author":"R. Banach","year":"1999","unstructured":"R. Banach and M. Poppleton. Sharp retrenchment, modulated refinement and simulation. Formal Aspects of Computing, 11:498\u2013540, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"3_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Retrenchment, refinement and simulation","author":"R. Banach","year":"2000","unstructured":"R. Banach and M. Poppleton. Retrenchment, refinement and simulation. In J. Bowen, S. King, S. Dunne, and A. Galloway, editors, Proc. ZB2000, volume 1878 of LNCS, York, September 2000. Springer."},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/BF00261259","volume":"16","author":"A. Blikle","year":"1981","unstructured":"A. Blikle. The clean termination of iterative programs. Acta Informatica, 16:199\u2013217, 1981.","journal-title":"Acta Informatica"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/BF00289066","volume":"11","author":"D. Coleman","year":"1979","unstructured":"D. Coleman and J.W. Hughes. The clean termination of pascal programs. Acta Informatica, 11:195\u2013210, 1979.","journal-title":"Acta Informatica"},{"key":"3_CR12","unstructured":"J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. In R. France, S. Gerhart, and M. Larrondo-Petrie, editors, WIFT\u201995: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. IEEE Computer Society Press."},{"key":"3_CR13","unstructured":"J.J. D\u2019Azzo and C.H. Houpis. Linear Control System Analysis and Design. McGraw-Hill, 4 edition, 1995."},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9780511663079"},{"key":"3_CR15","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"3_CR16","unstructured":"R.C. Dorf and R.H. Bishop. Modern Control Systems. Addison-Wesley, 1998."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"M. Dunstan, T. Kelsey, U. Martin, and S. Linton. Lightweight formal methods for computer algebra systems. In ISSAC\u201998: Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, Rostock, 1998. ACM Press.","DOI":"10.1145\/281508.281560"},{"key":"3_CR18","unstructured":"G.F. Franklin, J.D. Powell, and M.L. Workman. Digital Control of Dynamic Systems. Addison-Wesley Longman, 3rd edition, 1998."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys, 1991.","DOI":"10.1145\/103162.103163"},{"key":"3_CR20","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"John Harrison and Laurent Th\u00e9ry. A skeptic\u2019s approach to combining HOL and Maple. Journal of Automated Reasoning, 21:279\u2013294, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"3_CR22","unstructured":"F.B. Hildebrand. Advanced Calculus for Applications. Prentice-Hall, 1962."},{"issue":"10","key":"3_CR23","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576\u2013583, October 1969.","journal-title":"Communications of the ACM"},{"key":"3_CR24","unstructured":"D.S. Neilson. From Z to C: Illustration of a Rigorous Development Method. PhD thesis, Oxford University Programming Research Group, 1990. Technical Monograph PRG-101."},{"key":"3_CR25","unstructured":"K. Ogata. Modern Control Engineering. Prentice-Hall, 1997."},{"key":"3_CR26","first-page":"1","volume":"3","author":"O. Owe","year":"1993","unstructured":"O. Owe. Partial logics reconsidered: A conservative approach. Formal Aspects of Computing, 3:1\u201316, 1993.","journal-title":"Formal Aspects of Computing"},{"key":"3_CR27","unstructured":"P.N. Paraskevopoulos. Digital Control Systems. Prentice-Hall, 1996."},{"key":"3_CR28","unstructured":"E. Poll and S. Thompson. Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor. Technical Report 6-98, Computing Laboratory, University of Kent, May 1998."},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"M. Poppleton and R. Banach. Retrenchment: extending the reach of refinement. In ASE\u201999: 14th IEEE International Conference on Automated Software Engineering, pages 158\u2013165, Cocoa Beach, Florida, October 1999. IEEE Computer Society Press. Controlling Control Systems 61","DOI":"10.1109\/ASE.1999.802189"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"M. Poppleton and R. Banach. Retrenchment: Extending refinement for continuous and control systems. In Proc. IWFM\u201900, Springer Electronic Workshop in Computer Science Series http:\/\/ewic.org.uk\/ewic , NUI Maynooth, July 2000. Springer","DOI":"10.14236\/ewic\/IWFM2000.6"},{"key":"3_CR31","unstructured":"M.R. Poppleton. Formal Methods for Continuous Systems: Liberalising Refinement in B. PhD thesis, Department of Computer Science, University of Manchester, 2001."},{"key":"3_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/978-3-540-49676-2_20","volume-title":"More powerful Z data refinement: Pushing the state of the art in industrial refinement","author":"S. Stepney","year":"1998","unstructured":"S. Stepney, D. Cooper, and J. Woodcock. More powerful Z data refinement: Pushing the state of the art in industrial refinement. In J.P. Bowen, A. Fett, and M.G. Hinchey, editors, 11th International Conference of Z Users, volume 1493 of LNCS, pages 284\u2013307, Berlin, Germany, September 1998. Springer."},{"key":"3_CR33","series-title":"Lect Notes Comput Sci","first-page":"136","volume-title":"Frontiers of Combining Systems: Frocos 2000","author":"S. Thompson","year":"2000","unstructured":"S. Thompson. Integrating computer algebra and reasoning through the type system of Aldor. In H. Kirchner and C. Ringeissen, editors, Frontiers of Combining Systems: Frocos 2000, volume 1794 of LNCS, pages 136\u2013150. Springer, March 2000."},{"key":"3_CR34","unstructured":"J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice-Hall, 1996."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T12:01:44Z","timestamp":1587556904000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}