Using Alloy and UML/OCL to Specify Run-Time Configuration Management: A Case Study