Electrical microgrids are essential components for the energy transition, facilitating the integration of renewable sources and demanding robust, formally validated control strategies. The IEC 61850 architecture establishes itself as the fundamental standard for ensuring interoperability in these complex systems. To address this challenge, this paper proposes a methodology that uses Interpreted Petri Nets (IPNs) to model, validate, and implement the control logic for a microgrid compatible with this architecture. The developed formal model represents all operational modes, including autonomous, grid-connected, and fault, as well as the transitions between them, which are conditioned by the availability of energy resources (Utility, BESS, and DG) and the occurrence of grid disturbances. Formal validation, conducted through reachability analysis, state space exploration, and incidence matrix verification, demonstrated that the model possesses the desired properties: it is complete, safe, bounded, live, and free of deadlocks. The control logic extracted from the IPN model was then converted into Ladder language (IEC 61131-3) and tested in a CODESYS simulation environment, which emulates the operation of a Programmable Logic Controller (PLC). The experimental results confirmed a perfect match between the simulated behavior and practical operation, validating the proposed approach. This study consolidates IPNs as a reliable formal tool for the digitalization of microgrid control systems, ensuring a safe and verified transition from design to implementation.