| Summary: | 博士 === 元智大學 === 資訊工程學系 === 102 === The Programmable Logic Controller (PLC) is being integrated into the automation and control of computer systems in safety-critical domains at an increasing rate. Adequately testing ensures safety of such systems; thus, testing adequacy (i.e., test coverage) becomes an important research issue. Function Block Diagram (FBD) is a popular data-flow programming language for PLC and it is increasingly used in safety-critical applications. Current practice often involves translating an FBD program into an equivalent C program for testing. However, it cannot directly test a data-flow program, such as an FBD program, at the graphic (model) level. Furthermore, there are no commonly accepted structural test coverage criteria for data-flow programs. Therefore, this study first develops a new structural test coverage criterion, FB-Path Complete Condition Test Coverage (FPCC), for testing model-level FBD programs. The proposed testing scheme defines a complete test set for each function and function block in an FBD program. Moreover, this method augments the data-flow path concept with a sensitivity check to avoid fault masking and effectively detect logical function mutation errors.
In addition, the study designs an automatic test case generator, FPCCTestGen, for FPCC so as to enhance the practicability and acceptance of the FPCC approach. First, a supporting infrastructure for performing automatic FBD-to-UPPAAL-for-FPCC transformation is designed. Then, each input FBD, represented in PLCopen XML format, will be parsed and converted into corresponding UPPAAL model components. After that, queries related to FPCC characteristics are submitted to UPPAAL model checker for verification. Preliminary experiments show that this test coverage criterion is comprehensive and effective for error detection, and the generated test suite achieves the highest FPCC percentage with a near optimal number of test cases.
This study further presents a general FBD-to-UPPAAL transformation scheme, Function Block Model checking (FBM), by FPCCTestGen, so that model checking can be included in FBD verification process. Test cases based on a given test coverage criterion, such as decision coverage or condition coverage, can then be produced using a model checker. The empirical case study results show that the proposed FBD-to-UPPAAL transformation is valid and the incorporated model checking is beneficial.
The methods and tools developed in this study can enhance the effectiveness of testing and verification of data-flow programs.
|
|---|
