Verification and Optimization of a PLC Control Schedule

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    24 Citations (Scopus)
    193 Downloads (Pure)


    We report on the use of the SPIN model checker for both the verification of a process control program and the derivation of optimal control schedules. This work was carried out as part of a case study for the EC VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure. For this case study these techniques proved sufficient to verify the design of the controller and derive (time-)optimal schedules with reasonable time and space requirements.
    Original languageUndefined
    Title of host publication7th Int. SPIN Workshop on Model Checking of Software
    EditorsK. Havelund, J. Penix, W. Visser
    Place of PublicationBerlin
    Number of pages20
    ISBN (Print)3-540-41030-9
    Publication statusPublished - Aug 2000
    Event7th International SPIN Workshop on Model Checking and Software Verification 2000 - Stanford, United States
    Duration: 30 Aug 20001 Sept 2000
    Conference number: 7

    Publication series

    NameLecture Notes in Computer Science


    Conference7th International SPIN Workshop on Model Checking and Software Verification 2000
    Country/TerritoryUnited States


    • EWI-984
    • METIS-119632
    • IR-19109

    Cite this