High Availability (HA) is a quality of service that is required for many services, e.g. carrier grade services. Systems providing such services undergo upgrades, e.g. software version upgrade, like any other system. Avoiding/limiting service outage during these upgrades is of critical importance to meet the HA requirement. Thus, the upgrade campaign specifications, which drive the process need to be designed and evaluated properly. In this paper we discuss how modeling, automation and formal methods can help to design appropriate upgrade campaigns. We discuss our methods for upgrade campaign specification generation and evaluation with respect to the execution time and induced service outage.