This case study is concerned with the outpatient clinic and medical services from the information security, in particular confidentiality, perspective at the level of software architecture. The software architecture of the outpatient clinic management subsystem is modeled with Wright/c so as to specify and enable the static analysis of the confidentiality issues based on data flow over the architectural elements.
The complete information can be found in OutPatient_TechReport.pdf

You can get the ML description of the specification in OutPatient.ml