Declarative specification of system independent logic controller programs

The relationship between system independent logic controller programs (IEC standard 1131-3, Programmable Controllers, part 3: programming languages) and rule-based formal specifications is discussed. The Petri net and knowledge base theories can be joined together in the one context (Gentzen Logic). It combines the advantages taken from mathematical logic with the analysis power of Petri nets. The declarative specification, which is extracted from the description given in the initial standard IEC language (for example from structured text), can increase the efficiency of the logic controller program development. The well-structured specification, which is represented in the human-readable logic language, has direct impact on validation, formal verification and implementation of logic controller programs. The formality is introduced into the design technique, but it also can be used for post-design validations and maintenance. The symbolic deduction technique for PLC declarative program development appears very attractive. The CAD environment for application specific logic controllers is part of a research project at the University of Minho. The specification in the form of symbolic logic expressions may be verified, and then transformed into a format accepted by standard CAD tools (FPLD and FPGA compilers, VHDL tools)