Coordinating multiple drones for landing on vertiport-like infrastructures constitutes a general safety-critical swarm intelligence problem that combines discrete decision-making with domain-specific spatial occupancy constraints. Existing scheduling and control approaches often lack formal, executable correctness guarantees and remain loosely coupled to low-level control logic, making cyber-physical inconsistencies likely, especially when the number of drones increases. This work presents a formal and executable model for flight operation management of multiple tiny drones on multiple simplified vertiports based on bigraphical reactive systems. The proposed model captures both the spatial layout and the interactions among drones and the infrastructure, providing a unified understanding of a complex coordination problem. Compositionality enables the reconfiguration of takeoff and landing pad topologies, as well as fleet sizes, without altering the underlying rules. We employ model checking to generate the full state space from a set of initial states and verify safety invariants for 4 drones on a \(3\times 7\) grid, and 3 drones on a \(4\times 5\) grid. Landing success is formalized as a reachability condition. The compositional design of the specification facilitates reusability and modular verification, and the rule-based specification allows for execution of the traces of the proof.