Design of reactive control systems for event-driven operations

  • K. Lano
  • A. Sanchez
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


This paper explores the combination of formal methods with techniques taken from control engineering for specifying, designing and verifying reactive systems.

In particular, it is shown how to use techniques for specification and verification in VDM++ in combination with the synthesis of procedural controllers, a mathematical abstraction of the logic controlling an eventdriven sequential operation. The procedural controller is used as a provably correct specification of an event-driven operation to be implemented using VDM++. The resulting method enables a systematic approach for creating formalized designs of controllers for this type of operations, and proof obligations for the correctness of the designs against specifications to be generated. The approach is illustrated using an example.


Temporal Logic Finite State Machine Control Command Proof Obligation Dynamic Specification 
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.
    J. Abrial. The B Book: Deriving Programs from Meaning, Cambridge University Press, 1996.Google Scholar
  2. 2.
    M. Celiktin. Interval-based techniques for the specification and analysis of real-time requirements. Technical report, Universite Catholique de Louvain, 1994.Google Scholar
  3. 3.
    E. Durr, S. Goldsack, and J. van Katjwick. Specification of a cruise controller in VDM ++. In Proceedings of Real Time Workshop, ECOOP96, 1996.Google Scholar
  4. 4.
    J. Fiadeiro and T. Maibaum Describing, Structuring and Implementing Objects, in de Bakker et al., Foundations of Object Oriented languages, LNCS 489, Springer-Verlag, 1991.Google Scholar
  5. 5.
    K. Lano. Specification of a Chemical Process Controller in VDM ++ and B, ROOS Project Document GR/K68783-11, September 1996. Department of Computing. Imperial College, UK.Google Scholar
  6. 6.
    K. Lano, J. Bicarregui and A. Sanchez. Using B to Design and Verify Controllers for Chemical Processing, B Conference, IRIN, Nantes, France, 1996.Google Scholar
  7. 7.
    K. Lano, G. Goldsack, J. Bicarregui and S. Kent. Integrating VDM ++ and RealTime System Design, Z User Meeting, 1997.Google Scholar
  8. 8.
    I. Moon, G. Powers, J. R. Burch and E. M. Clarke, Automatic Verification of Sequential Control Systems using Temporal Logic, American Institute of Chemical Engineers (AIChE) Journal, 38(1):67–75, January 1992.Google Scholar
  9. 9.
    A. Sanchez and S. Macchietto. Design of Procedural Controllers for Chemical Processes, Computers and Chemical Engineering, 19, 5381–5386, 1995.Google Scholar
  10. 10.
    N. Alsop, L. Camillocci, A. Sanchez and S. Macchietto. Synthesis of Procedural Controllers — Application to a batch plant, Computers and Chemical Engineering, 20, S1481–S1486, 1996Google Scholar
  11. 11.
    A. Sanchez. Formal Specification and Synthesis of Procedural Controllers for Process Systems. Springer-Verlag. Lecture Notes in Control and Information Sciences, vol. 212. 1996.Google Scholar
  12. 12.
    M. Schenke and A. Ravn. Refinement from a Control Problem to Programs, in J. Abrial, E. Börger and H. Langmaack (Eds.), Formal Methods for Industrial Applications, Lecture Notes in Computer Science Vol. 1165, Springer-Verlag, 1997.Google Scholar
  13. 13.
    G. E. Rotstein, A. Sanchez and S. Macchietto. Procedural Control of Discrete Event Systems, Submitted to J. Discrete Event Systems, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • K. Lano
    • 1
  • A. Sanchez
    • 2
  1. 1.Dept. of ComputingImperial CollegeLondon
  2. 2.Centre for Process Systems EngineeringImperial CollegeLondon

Personalised recommendations