Support fo the development of the model checker TAPAAL

TAPAAL is a Petri net-based model checker designed for verifying and synthesizing complex concurrent systems with real-time and data structure support. It has demonstrated significant utility in applications like real-time workflow analysis and network update synthesis, earning accolades such as three gold and two silver medals at the 2022 Model Checking Contest. Despite its success in research projects like QASNET and WHAT-IF, which drove theoretical advancements, TAPAAL faces challenges due to insufficient funding for code development, leading to fragmented code branches and prototype implementations that need consolidation and testing for user accessibility. Continued development requires a dedicated team, including student programmers, to maintain and enhance the codebase, ensuring a stable, user-friendly version. Without financial support, TAPAAL’s potential to impact industrial verification of safety-critical real-time systems may remain unrealized, limiting its ability to improve system safety and dependability.