Design of verified logic control programs

To complement the largely manual design of logic control programs in industrial practice, this contribution proposes a method for systematically (and partly algorithmically) deriving logic controllers for given specifications. The main idea is to structure the information available for the design in form of specific intermediate formats which are iteratively refined and straightforwardly lead to controllers formulated as Sequential Function Charts. To analyze whether the design complies with all given specifications, model-based verification is applied subsequently, i.e. the controller is converted into timed automata, the latter are composed with a plant model, and model-checking algorithmically verifies (or falsifies) logic properties for the composed system. The procedure is described here for the example of a multi-product batch plant.