Most formal methods see the correctness of a software system as a binary decision. However, proving the correctness of complex systems completely is difficult because they are composed of multiple components, usage scenarios, and environments. We present QuAC, a modular approach for quantifying the correctness of service-oriented software systems by combining software architecture modeling with deductive verification. Our approach is based on a model of the service-oriented architecture and the probabilistic usage scenarios of the system. The correctness of a single service is approximated by a coverage region, which is a formula describing which inputs for that service are proven to not lead to an erroneous execution. The coverage regions can be determined by a combination of various analyses, e.g., formal verification, expert estimations, or testing. The coverage regions and the software model are then combined into a probabilistic program. From this, we can compute the probability that under a given usage profile no service is called outside its coverage region. If the coverage region is large enough, then instead of attempting to get 100% coverage, which may be prohibitively expensive, run-time verification or testing approaches may be used to deal with inputs outside the coverage region. We also present an implementation of QuAC for Java using the modeling tool Palladio and the deductive verification tool KeY. We demonstrate its usability by applying it to a software simulation of an energy system.

翻译：摘要：大多数形式化方法将软件系统的正确性视为二元决策。然而，完全证明复杂系统的正确性十分困难，因为此类系统由多个组件、使用场景和环境构成。我们提出QuAC——一种通过结合软件架构建模与演绎验证来量化面向服务软件系统正确性的模块化方法。该方法基于面向服务架构模型及系统的概率使用场景。单个服务的正确性通过覆盖区域近似描述，该区域是一个公式，用以说明该服务的哪些输入已被证明不会导致错误执行。覆盖区域可通过多种分析手段（如形式化验证、专家评估或测试）联合确定。随后将覆盖区域与软件模型整合为概率程序，据此可计算在给定使用场景下所有服务均在其覆盖区域内被调用的概率。若覆盖区域足够大，则可避免追求可能代价过高的100%覆盖率，转而采用运行时验证或测试方法处理覆盖区域外的输入。我们还展示了QuAC在Java平台上的实现，该实现使用建模工具Palladio与演绎验证工具KeY。通过将其应用于能源系统软件仿真，验证了该方法的可用性。