Formal Modeling of Testing Software for Cyber-Physical Automation Systems

The paper presents a framework which uses formal models for testing control software for industrial automation systems. The formalism called Net Condition/Event Systems (NCES) is applied to model the program under test, along with the system under control (plant) and the testing environment. The benefits of using the framework include the opportunities to test systems with time delays without the need to wait, to test parameterized sets of systems with a single execution of a test suite, and to check test suites for correctness. The use of the framework is illustrated on a simple system consisting of a lab-scale plant and a control application for it.