Software specifications play an important role in the software design process and are of great significance for improving software quality. Especially in the textile industry, with the rapid development of intelligent manufacturing, the complexity of control software for automated weaving machinery and textile production lines is increasing, making the formal verification of these systems essential. The finite state automata (FSA) generated by existing automatic specification mining methods still have insufficient accuracy in handling large-scale systems. In order to improve the accuracy of FSA, this paper proposes a deep specification mining method based on invariants and model checking. In this method, firstly, we use the Transformer model to generate feature values. Then, based on the different data types of the target library, different clustering algorithms were selected to cluster and generate the initial FSA. Afterwards, the optimal FSA of the F-measure was chosen, and the invariant formula was constructed by mining the information of potential invariants. Finally, refine the FSA through model checking. The refinement process is achieved by adding or removing transformation rules and states on the overall FSA based on the invariant formula. The proposed method provides a reliable solution for mining the behavioral specifications of complex logic systems in textile machinery, ensuring the stability of industrial control software. The effectiveness of our method was evaluated through 11 target library classes, and experimental results showed that the average F-measure of our proposed method can reach 97.06%, which is 25.09% higher than the average F-measure of the DSM.

software specification, finite state automata, transformer, model checking, textile industrial software