eHRM. EHealth Management Record
eHRM was developed as part of a case study proposed by industrial partners in an ongoing European project (NeSSOS). For more information, visit: eHRMApp.
You can download the data model from here. (The syntax used is the sintax of ActionGUI data model. More over, the list of data invariants are available here. Each inviariant has a name associated. Finally, the SMT-LIB files generated by the tool are here.
Note: As we mention in the paper, we use Z3 versions 4.3.1 and 4.3.2 to check the properties. If you download the examples, you can see two folders, "GROUP1" and "GROUP2", for the first group we use Z3 version 4.3.1 and for the second, Z3 version 4.3.2.
More people involved in this project: Manuel Clavel.