A Programmable Logic Controller (PLC) is an essentially domain-specific computer used to control physical equipment and is widely used in industrial control fields. It plays a crucial role in automating complex processes for industrial automation systems, requiring high reliability as code vulnerabilities can potentially lead to disasters. Therefore, vulnerability detection in PLC programs is of significant importance. However, the availability of tools supporting vulnerability detection in PLC programming languages is limited. This paper attempts to improve industrial security from the perspective of code security and proposes a static code analysis approach specifically designed for IEC 61131–3 Structured Text (ST) programs. This approach uses structural pattern matching and symbolic execution technology to identify program defects and improve quality by detecting problematic code structures and potential issues early in the development process, thereby reducing the debugging effort required during developments. Considering the characteristic of periodic loop execution in PLCs, we introduce the loop unwinding technique to collect constraints from subsequent execution cycles for detection purposes. Based on the aforementioned approach, we implement a static code analysis tool, ST-Checker and make a series of evaluations. The experimental results show that this method is feasible and can detect potential defects that existing PLC compilers cannot detect, improving the precision of defect detection with data dependencies.

Programmable Logic Controllers (PLCs) are specialized computers extensively utilized in industrial control fields. Since they control industrial equipment, software faults in PLCs can result in significant losses. However, current testing for PLC programs is mainly manual, and there are very few automatic testing tools. Structured Text (ST) is one of the five PLC programming languages stipulated by the IEC 61131-3 standard, suitable for writing complex control logic. This paper proposes an automatic unit test case generation framework for ST programs based on Dynamic Symbolic Execution and PLC states, as well as a supporting algorithm, and implements the PLCAutoTester tool. PLCAutoTester supports the automatic generation of ST program unit test cases that comply with statement coverage, branch coverage, and MC/DC coverage criterion. We evaluated the PLCAutoTester using 20 PLC programs and compared it with S${}_{YM}$PLC. The experimental results show that PLCAutoTester can generate unit test cases with high coverage in a short time. And in 11 common programs, PLCAutoTester is able to generate test cases with almost the same statement coverage as S${}_{YM}$PLC while reducing the number of test cases by 95%.

The excellent model obtained through natural data training in deep learning is easily tampered with by adversarial examples. After discovering that, adversarial training has become the best way to defend against adversarial attacks and improve the robustness of the model. Since it is expensive to frequently calculate adversarial examples in each epoch during the training process, most people prefer to choose a single-step adversarial training method. However, the single-step adversarial training method will cause catastrophic overfitting and make the model lose robustness forever. In this paper, we explain adversarial training from the perspective of data augmentation, using artificial binary data to explore the reason for the occurrence of this overfitting. We propose two methods, VFSAT(Various fixed-stepsize single-step adversarial training) and GradSum, to prevent the overfitting in term of local smoothing and improve the robustness of the model obtained by single-step adversarial training. Simultaneously, experiments on CIFAR-10 and Tiny ImageNet datasets were constructed and the proof that single-step adversarial training could also resist multi-step adversarial attacks was derived.

SysML state machine (SysML-STM) is a modeling tool used in the Systems Modeling Language (SysML) to describe the behavior of a system. It is widely used in model-driven development (MDD). Formal methods are mathematical techniques to ensure the correctness, reliability and safety of software systems and hardware designs. In this paper, we introduce formal methods into MDD by transforming a SysML-STM model into a Uppaal timed automata. By formally verifying the system at an early stage of the development life-cycle, we aim to enhance the system's robustness. We design the mapping rules between the two models and have developed a tool, STMTU, to transform them directly. Our tool effectively leverage the benefits of formal verification techniques to ensure the correctness and reliability of the system. And the direct transformation of these models not only reduces the learning cost for developers but also helps to promote the wider adoption of formal methods.

There are quite tight timing requirements in deterministic low latency network. The IEEE 802.1 Time-Sensitive Networking (TSN) task group has proposed several traffic shapers to satisfy real-time communications requirements. Traditionally, the performance of TSN is analyzed by simulations, whereas these methods cannot cover all corner cases. This paper firstly presented formal models of the TSN’s time-aware and peristaltic shapers using UPPAAL, tactically solving the problem mentioned above. Afterward, we verified some properties of the shapers models, of which the results could evaluate whether these shapers are able to satisfy strict timing requirements or not. Based on the models, we can discuss about the performance of time-critical traffic combining the preemption mechanism. More-over, we can also analyze resource utilization and transmission latency. Under the time properties analysis and verification of TSN traffic shapers, we can provide engineers with an accessible reference that may assist them in developing the TSN.

Since programmable logic controllers (PLCs) control safety-critical infrastructures, examining the PLC software satisfies the high-reliability specifications necessary to ensure the safeness of PLCs.However, prior works have limitations in finding defects in the PLC source code.Static verification techniques suffer from notable false positives without capturing runtime behavior.The symbolic execution and conformance testing technique captures the relations of inputs and outputs.It is not sufficient to consider only the data constraints as the PLC operates in real-time.In this paper, we propose a novel approach in the detection of the runtime behavior of PLC programs with incorporated time constraints.This testing approach automatically finds implementation errors in PLC programs by mining invariants from runtime traces.As the existing tools mine only data or time invariants which are inadequate to test PLC programs, our approach focuses on the interplay of data and time invariants.Dynamically detected datatime invariants are then checked with the safety specifications.We evaluate the usefulness of our approach in a real-life case.The experimental results show that the proposed approach can find errors in PLC programs effectively.