Research on Task-based Requirements Modeling and Compositional Verification for Automated Processing System

Formal verification is playing an increasingly important role in the development of safety-critical systems, such as signal process systems. Through formal modeling and verification, the behavior and decision-making processes of safety-critical systems can be described more precisely, thereby ensuring the safety of the system. By utilizing formal models, comprehensive verification of these models can be conducted to identify and fix potential errors and defects in the early phase. However, as the scale of systems increases, the complexity of formal verification models correspondingly increases, potentially resulting in verification failures. To address this issue, this paper proposes a task-based requirements modeling and compositional verification approach for signal process systems. It reduces the complexity of formal verification models by only considering task related requirements. This approach not only effectively identifies task related errors but also ensures a certain level of verification efficiency. We also conduct a practical case study on an automated processing system to demonstrate the validity of our approach.