Article’s

Automated irrigation systems are critical for efficient water and nutrient management in modern agriculture. However, most existing approaches rely on heuristic methods without formal verification, leaving the system prone to deadlocks or inconsistent operation. This paper addresses this research gap by presenting a formal modeling and verification of an automatic irrigation system using Petri Nets. The system autonomously monitors soil moisture and nutrient levels to perform irrigation and fertilization without human intervention. The workflow including sensing, decision-making, actuation, logging, and notification was modeled and simulated using PIPE 4.3.0 and WoPeD 3.8.0, providing both formal analysis and intuitive workflow visualization. Verification of reachability, boundedness, liveness, safeness, and deadlock-freeness confirms reliable system operation, highlighting the relevance of Petri Net-based modeling for robust, scalable autonomous irrigation systems.