Statistical Model Checking meets GDPR

Software systems are incorporated into various aspects of human society. However, their integration brings a set of challenges, especially when software operates on personal data. The systems must be correct and provide the desired functionality while maintaining privacy and security of personal data. Verification techniques can support software system development and provide mathematical evidence of their correctness and security. This work considers two recent applied and collaborative national/EU projects from different domains. Both projects involve processing personal data and sharing it among multiple individuals and organizations. Therefore, ensuring security and data privacy guarantees, as mandated by the General Data Protection Regulation (GDPR), is crucial. We explore the applicability of formal methods and demonstrate the utility of Statistical Model Checking to ensure security and privacy in real-world projects. The goal is to validate specific aspects of GDPR compliance for both projects.