Z/Alloy formal specification for client identifying data regulation for banks in Switzerland
This project contains the formal specification of CID FINMA regulation. The specification is written using the Z notation and Alloy and was developed by Serge (Siarhei Vinahradau, vinahradau@yahoo.de).
The CID FINMA regulation was published by the Swiss Financial Market Supervisory Authority (FINMA) and describes the requirements to handling client identifying data (CID) by banks in Switzerland (S. References below). The document is available in German.
This Z specification can be animated using the jaza animator. Jaza is available for download as an executable on github, thanks to Mark Utting (S. References).
The Alloy specification can be executed within the Alloy Analyzer GUI.
FINMA-Rundschreiben „Operationelle Risiken – Banken“ (published in 20.11.2008, last updated in 2017). https://www.finma.ch/de/~/media/finma/dokumente/rundschreiben-archiv/finma-rs-200821---30-06-2017.pdf
Jaza Animator: https://github.com/uho/jaza
CZT IDE: http://czt.sourceforge.net/
Alloy Analyzer: https://alloytools.org/