A FORMAL APPROACH ON SPECIFICATION MODELING TO SUPPORT INDUSTRIAL PLC PROGRAM VERIFICATION

Intensive global competition requires the automotive manufacturers to launch new vehicle models with a shorter launch time, better quality, lower cost and more customization. One of the key enablers for achieving these objectives is to have an efficient & error-free manufacturing automation system which is typically controlled by Programmable Logic Controllers (PLC). The current PLC logic code testing process in automotive industry is usually performed manually by individual engineer, and the overall testing quality highly depends on the engineer's expertise and experience. The PLC logic code testing normally consists of two parts, testing requirements (specification) and testing methods. One of the major hurdles for applying rigorous testing methods on PLC logic verification in industry is the lack of formal testing specifications. The current PLC testing specifications and requirements are documented in various formats, such as sequence of operation document, process instrument diagram, wiring diagrams, and time motion diagrams, etc. These varied documents cannot be directly used for control logic testing and require a better alternative. Formal methods, the latest technology widely used in software testing, is an approach selected for generating comprehensive test cases to ensure the correctness and consistency of PLC programs. This paper presents a novel approach for specifying the expected behavior of the already implemented industrial PLC code. The generated formal specification models can work with math-based logic verification tool to facilitate the usage of formal verification in manufacturing automation control. The specification modeling methodology contains all the required information from different logic design and testing phases, such as process sequence, wiring information, logic pattern, code comments, and domain knowledge, etc. And the statecharts is used as model formalism, because of its capability to model states hierarchically and provide a better visual representation.