The healthcare sector is increasingly recognising cybersecurity as an integral part of patient safety. In recent years, healthcare computer networks have been severely affected by numerous large-scale cyberattacks that have exposed fundamental security gaps in network architectures. As a result, governments and regulatory organizations have introduced comprehensive cybersecurity standards and cyberdefense strategies for healthcare infrastructure. In this paper, we develop a security requirements specification for a healthcare computer network and present a combined approach to formally model and verify it using Alloy and TLA \(^{+}\) . With Alloy, we analyse the structural constraints, which include network segmentation, the security lattice, and access control rules. In TLA \(^{+}\) , we verify temporal correctness properties, with particular emphasis on dynamic reconfiguration, state-based monitoring, and the isolation of critical devices during cyberattacks. By integrating two state-based methods, we demonstrate how both static and dynamic security properties can be analysed within a unified framework, enabling the formal verification of cybersecurity requirements for critical infrastructure.