This is a case study for the specification and verification of a software architecture called Project IT .
The software system supports data exchange, in the context of a project called ProjectIT, between a customer and a consortium formed by two companies: a software vendor that develops an application software for the customer, and a hardware vendor that supplies the hardware platform for the software. The complete information can be found in ProjectIT.pdf

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