Controlling Control Systems: An Application of Evolving Retrenchment

  • Michael Poppleton
  • Richard Banach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


We review retrenchment as a liberalisation of refinement, for the description of applications too rich (e.g. using continuous and infinite types) for refinement. A specialisation of the notion, evolving retrenchment, is introduced, motivated by the need for an approximate, evolving notion of simulation. The focus of the paper is the case study, a substantial second-order linear control system. The design step from continuous to zero-order hold discrete system is expressible as an evolving retrenchment. Thus we demonstrate that the retrenchment approach can formalise the development of useful applications, which are outside the scope of refinement. The work is presented in a data type-enriched language containing the B language of J.-R. Abrial.


Operation Sequence Concrete Model Proof Obligation Discrete State Space Abstract Input 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    K.E. Atkinson. An Introduction to Numerical Analysis. Wiley, 1989.Google Scholar
  2. [2]
    R. J. R. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.Google Scholar
  3. [3]
    R.J.R. Back and M. Butler. Fusion and simultaneous execution in the refinement calculus. Acta Informatica, 35:921–949, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    R. Banach. Maximally abstract retrenchments. In Proc. IEEE ICFEM2000, pages 133–142, York, August 2000. IEEE Computer Society Press.Google Scholar
  5. [5]
    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–147, Montpellier, France, April 1998. Springer.Google Scholar
  6. [6]
    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.Google Scholar
  7. [7]
    R. Banach and M. Poppleton. Retrenchment and punctured simulation. In K. Araki, A. Galloway, and K. Taguchi, editors, Proc. IFM’99:Integrated Formal Methods 1999, pages 457–476, University of York, June 1999. Springer.Google Scholar
  8. [8]
    R. Banach and M. Poppleton. Sharp retrenchment, modulated refinement and simulation. Formal Aspects of Computing, 11:498–540, 1999.zbMATHCrossRefGoogle Scholar
  9. [9]
    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.Google Scholar
  10. [10]
    A. Blikle. The clean termination of iterative programs. Acta Informatica, 16:199–217, 1981.zbMATHCrossRefMathSciNetGoogle Scholar
  11. [11]
    D. Coleman and J.W. Hughes. The clean termination of pascal programs. Acta Informatica, 11:195–210, 1979.zbMATHCrossRefGoogle Scholar
  12. [12]
    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’95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. IEEE Computer Society Press.Google Scholar
  13. [13]
    J.J. D’Azzo and C.H. Houpis. Linear Control System Analysis and Design. McGraw-Hill, 4 edition, 1995.Google Scholar
  14. [14]
    W.-P. de Roever and K. Engelhardt. Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998.Google Scholar
  15. [15]
    E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.Google Scholar
  16. [16]
    R.C. Dorf and R.H. Bishop. Modern Control Systems. Addison-Wesley, 1998.Google Scholar
  17. [17]
    M. Dunstan, T. Kelsey, U. Martin, and S. Linton. Lightweight formal methods for computer algebra systems. In ISSAC’98: Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, Rostock, 1998. ACM Press.Google Scholar
  18. [18]
    G.F. Franklin, J.D. Powell, and M.L. Workman. Digital Control of Dynamic Systems. Addison-Wesley Longman, 3rd edition, 1998.Google Scholar
  19. [19]
    D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys, 1991.Google Scholar
  20. [20]
    M.J.C. Gordon and T.F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
  21. [21]
    John Harrison and Laurent Théry. A skeptic’s approach to combining HOL and Maple. Journal of Automated Reasoning, 21:279–294, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  22. [22]
    F.B. Hildebrand. Advanced Calculus for Applications. Prentice-Hall, 1962.Google Scholar
  23. [23]
    C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, October 1969.zbMATHCrossRefGoogle Scholar
  24. [24]
    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.Google Scholar
  25. [25]
    K. Ogata. Modern Control Engineering. Prentice-Hall, 1997.Google Scholar
  26. [26]
    O. Owe. Partial logics reconsidered: A conservative approach. Formal Aspects of Computing, 3:1–16, 1993.Google Scholar
  27. [27]
    P.N. Paraskevopoulos. Digital Control Systems. Prentice-Hall, 1996.Google Scholar
  28. [28]
    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.Google Scholar
  29. [29]
    M. Poppleton and R. Banach. Retrenchment: extending the reach of refinement. In ASE’99: 14th IEEE International Conference on Automated Software Engineering, pages 158–165, Cocoa Beach, Florida, October 1999. IEEE Computer Society Press. Controlling Control Systems 61Google Scholar
  30. [30]
    M. Poppleton and R. Banach. Retrenchment: Extending refinement for continuous and control systems. In Proc. IWFM’00, Springer Electronic Workshop in Computer Science Series, NUI Maynooth, July 2000. Springer
  31. [31]
    M.R. Poppleton. Formal Methods for Continuous Systems: Liberalising Refinement in B. PhD thesis, Department of Computer Science, University of Manchester, 2001.Google Scholar
  32. [32]
    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–307, Berlin, Germany, September 1998. Springer.Google Scholar
  33. [33]
    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–150. Springer, March 2000.Google Scholar
  34. [34]
    J. Woodcock and J. Davies. Using Z: Specification, Refinement and Proof. Prentice-Hall, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Michael Poppleton
    • 1
  • Richard Banach
    • 2
  1. 1.Department of ComputingOpen UniversityMilton KeynesUK
  2. 2.Department of Computer ScienceManchester UniversityManchesterUK

Personalised recommendations