Ett datadelningsavtal (DSA) är ett avtal mellan två eller flera huvudmän som reglerar hur de delar data. Avtal är vanligtvis representerade som en uppsättning klausuler som uttrycks med hjälp av deontiska begreppen skyldighet, förbud och tillstånd. I den här artikeln presenterar vi hur man modellerar DSA med hjälp av Event-B specifikationsspråket. Avtalsklausuler är modellerade som temporal-logiska formler som bevarar den intuitiva betydelsen av deontiska operatörer, och begränsar de åtgärder som en huvudman kan utföra. Vi har utnyttjat ProB-animatorn och modellkontrollen för att verifiera att ett system beter sig enligt dess tillhörande DSA och för att bekräfta att huvudmännens åtgärder är i överensstämmelse med DSA-klausulerna.
I REF presenterar författarna en formalisering av DSA-klausuler i Event-B och ProB-animator och modellkontroll utnyttjas för att verifiera att ett system beter sig enligt dess tillhörande DSA.