Abstarct: Swarm robotic (SR) draws inspiration from nature and is emerged as a synthesis of swarm intelligence and robotic. Due to special properties like flexibility, robustness, and scalability, swarm robotic has several advantages in comparison to other multi robot systems. On the other hand, SR properties and characteristics expand swarm robotic applications domain to dangerous, industrial and military environments. Hence, scientists had a special interest in swarm robotic in the last years. Lack of common control software makes it difficult to analyze, maintain or verify swarm robotic systems. Using formal methods for SR modeling and design almost contributes to overcoming these problems. However, there is no guarantee that the implementation matches the system requirements and specifications in formal methods too. The proposed approach is using supervisory control theory (SCT) as system modeling and design tool. This theory addresses the problem of the formal methods with automatic generation of control codes. One of the well-known tasks of swarm robotic is foraging inspired by ant’s seed searching. Foraging as a combination of multiple subtasks like collective searching, collective transport, and task allocation is considered as one of the most complex tasks of swarm robotic. In this dissertation, a foraging task is designed and implemented. For this purpose, a comprehensive tool is proposed which gets system behavior and requirements as generators and produces desired control code automatically. The proposed tool uses a more powerful version of SCT named ptSCT that adds probability and time elements to SCT. Demonstrating the power of ptSCT, two tasks namely obstacle avoidance and synchronization of robots are designed, and implemented using both SCT and proposed ptSCT. For evaluation of implemented foraging, more than 2400 experiments are heavily tested on ARGoS simulation environment with E-puck robot. Effect of the number of targets, obstacles, and robots are evaluated. Moreover, the effect of resting of robots on the system performance is also considered. The experimental results declare the advantages of the ptSCT, in terms of simplicity, reusability, and automatic code generation. Therefore, ptSCT can tackle other SR tasks modeling.