Formal proofs for QoS-oriented Transformations

The methodology of Model Driven Architecture (MDA) has been a popular area of research in recent years. To cater for the increasing awareness of the importance in software Quality of Service (QoS), some have suggested MDA as a solution. However, unlike functional properties, QoS displayed in a development cycle is prone to changes after deployment due to a non-constant runtime environment and usage. A possible solution is to provide a monitoring framework to ensure that QoS violations are always detectable. However, as with any MDA based approach it is dangerous to simply assume that transformations will do exactly as specified. This paper describes an approach for producing formal proofs for our particular QoS-oriented transformational system[1], based on the proof-as-programs methodology.