Enabling interoperability is a challenging task in medical data exchange and is often addressed by the use of versatile communication standards like HL7 FHIR. Although daily routine and scientific experiences show its suitability, the use comes with major risks regarding safety and security of data. To overcome these problems, we present an approach to enable a formal verification of medical communication use cases. We identified the Neonatal Screening as a practical example in which two process participants (physician and screening laboratory) are involved. We analyzed the FHIR specification as well as identified necessary resources in that context and formally modeled them as algebraic specifications. By that, we were able to represent the participants’ behavior and data flow with help of Algebraic Petri Nets. This strategy allows to formally verify the correctness of a system by specified requirements regarding data safety and data security.