An Innovative Formal Verification Method Based on Timed Petri Nets With Integrated Database Tables
提出一种基于时间Petri网与数据库表的形式化验证方法，通过扩展时序逻辑处理数据流，将系统正确性验证转化为公式可满足性问题，并用案例验证了有效性。
Formal verification becomes increasingly critical to ensure system functionality, reliability and safety as they grow in complexity. Existing methods tend to focus on a single dimension of system aspects—such as control flow, data flow or timing constraints—or, at most, consider two of these perspectives without integrating all three. In addition, data flow models generally represent high-level data abstraction without including operational details within underlying contexts. The inability of these models to capture system behavior undermines their reliability, ultimately increasing the likelihood of the corresponding systems malfunctioning. To address these issues, we propose a formal verification method based on a timed Petri net with database tables (TPDT-net). First, we model the system using TPDT-net and generate its state reachability graph (SRG). Next, we extend timed computation tree logic (TCTL) by introducing database-related data element operators, thus proposing a database-oriented TCTL (DTCTL) model checking method. In addition, we formalize the system correctness problem as corresponding DTCTL formulas, which are analyzed based on the SRG. This approach transforms correctness verification into a satisfiability problem of DTCTL formulas within the SRG. Finally, we validate the practicality and effectiveness of the proposed method through case studies and experiments.