SMT SOLVERS APPLICATION FOR FORMAL VERIFICATION OF POLICY-BASED SERVICES IN CLOUD ENVIRONMENTS
DOI:
https://doi.org/10.34185/1991-7848.itmm.2023.01.074Keywords:
SMT, automated Reasoning, cloud technologies, formal verificationAbstract
Formal verification of policy-based services in cloud environments using SMT (Satisfiability Modulo Theories) solvers involves encoding the policies and service behaviors as logical formulas and checking whether the formulas are satisfactory or unsatisfiable. SMT solvers can be used to verify that the policies are enforced correctly and that the service behaviors are consistent with the policies.
References
Zhang, X., Sun, M. (2019). SMT-Based Modeling and Verification of Cloud Applications. In: Xia, Y., Zhang, LJ. (eds) Services – SERVICES 2019. SERVICES 2019. Lecture Notes in Computer Science(), vol 11517. Springer, Cham.
L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340, 2008.
