Alloy Assignment - Modeling HIPAA

Due at 6:00PM on Thursday April 30, 2009 via Catalyst Collect It

The Health Insurance Portability and Accountability Act of 1996 (HIPAA) Privacy Rule "provides federal protections for personal health information held by covered entities and gives patients an array of rights with respect to that information. At the same time, the Privacy Rule is balanced so that it permits the disclosure of personal health information needed for patient care and other important purposes."*

More information about HIPAA can be found at:

Like many other situations, figuring out precisely what is and is not permitted is a complicated issue facing software developers who are dealing with HIPAA regulations - failure can be costly both to organizations that can face penalties for non-compliance and also to individuals whose personal health information is misused.

Can Alloy help induce clarity among some key aspects of the HIPAA tarpit?

Your assignment is to create a model to explore this issue, specifically the right to access patient's health information. You should, at a minimum, model:

  1. Individuals
  2. Personal representatives of individuals (for example, parents of minors)
  3. Patient information that your health care providers can share with each other
  4. Patient information that your health care providers can share externally only with your explicit authorization
  5. Patient information that your health care provider may not share with you - specifically, psychotherapy notes (although these can by shared externally only if you explicitly authorize it).

You must also define several assertions (say 3-5, perhaps more) that you think should be true but were not specified as facts.  This is a key part of the assignment, as it will help you build your understanding of your own model.

There is much more to HIPAA - for instance, handling subpoenas, information used for research, employment information, etc. - but these are not required to be dealt with in your model.  Neither are dynamic models -- those that perform operations such as requesting authorization, changing personal representatives, etc.

The intent of the assignment is to learn about Alloy more than about HIPAA, although some of that is needed of course. Therefore, you should turn in not only your "final" model, but also a sequence of your intermediary models and descriptions about what information (counterexamples, for example) you learned at these intermediate steps that helped your iterate to your final model. You are encouraged to write inline comments to provide information about what your lines of code mean and why you made that decision. You must also provide a brief (say, 2-3 paragraph) analysis of your reactions to Alloy and the supporting tools.  If you work in a group, you should each write this analysis individually, but place them all in the same turn-in packet (and mark whose is whose).

Alloy can be downloaded from, and a very nice tutorial can be found at

Turn in your code and acoompanying files to Catalyst Collect It (UW NetID required) by 6:00PM on Thursday April 30, 2009. Please send any questions or concerns to suporn@cs.