Component Based Modeling Method For PLC Control Softwares

Embedded systems are widely used in many safety critical fields. The correctnessand reliability of embedded systems have significant influence on human safety, socialdevelopment and society steady. It is also an important research topic in computer scienceand automatic control. Formal method is an important way to ensure the correctness andreliability of embedded systems. However, formal method is based on mathematicaltheory and hard to learn. This hinders the applications of formal method in industry.This dissertation investigates the component-based modeling method for PLC soft-ware. Considering the characteristics and practical problems of PLC software, the methodcontains three levels: modeling language, consistency checking and implementation. Themain contributions are summarized as follows:1. The modeling language level provides a domain specific modeling language PLC-BIP. PLC-BIP extends BIP with two aspects. One is domain knowledge expression,and the other is concept annotation. The PLC features, such as cyclic executionmechanism, timer, function call and interruption scheduling are studied and mod-eled as component. It suggests top down general decomposition principles, andbottom up components mapping architecture for PLC systems. It defines the op-erational semantics for IL language, and provides a modeling method for exitingprograms using translation.2. The checking level provides a static checking framework based on domain knowl-edge for the problem that models may violate the potential domain constraints.It provides a formal expression for domain constraints. The constraints checkingproblem is converted to the concept lattice constraints solving problem. The check-ing is automatically executed whiling modeling, and can find errors more earlier.3. The implementation level presents a method for PLC code synthesis based on for-mal models. The method considers the realistic feature of hardware and the real-time and resource constraints. This makes the synthesis method more practical. Itprovides an algorithm of the method and show the synthesis steps by a two-doorcontrol case.4. A modeling prototype for the domain knowledge and component-based modeling method is implemented. It provides a graphic editor, a library for device controldomain and a compiler with the functions of syntax and semantic checking. Italso supports the domain concept annotation and domain constraints checking. Acase study about the modeling methodology for gate control system of LingShanBuddhist Palace in Wuxi is presented. It illustrates the PLC-BIP language providesan easier way for the modeling process by component types and domain operators.The automatic checking method of domain constraints is applied and shows itsefciency.