Reusable Requirements in Automated Verification of Distributed Systems
The growing popularity of infrastructure-as-a-service cloud computing, software-defined networking, and related technologies have enabled the rapid creation of complex, large-scale distributed systems. Many of these systems are used by applications with stricter requirements than those covered by SLAs, such as those used by the financial, healthcare, and industrial sectors. Mathematical methods exist which can be used to formally verify many of these safety, liveness, and security properties, but are rarely used by system designers. In this paper, the authors identify brittle requirements as one of the problems which impede the use of formal methods in distributed system design, and propose a solution based on the decomposition of a formal model into a user-defined component and one or more domain abstractions.