Modular verification of web services using efficient symbolic encoding and summarization
AssigneeNEC Laboratories America, Inc.
InventorsChao Wang, Fang Yu, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
A system and method for verifying a composition of interacting services in a distributed system includes generating a concurrent process graph (CPG) for processes in a system and symbolically encoding the CPG of each process to perform a reachability analysis. Symbolic summaries are generated for concurrently running processes based on the reachability analysis. Modular verification is conducted by utilizing the symbolic summaries of the processes to verify a system of interrelated processes.
Claims23
A method for verifying a composition of interacting services in a distributed network system, comprising:
- generating a concurrent process graph (CPG) for processes in a system;
- symbolically encoding the CPG of each process to perform a reachability analysis;
- generating symbolic summaries for concurrently running processes based on the reachability analysis;
- and
- conducting modular verification by utilizing the symbolic summaries of the processes to verify a system of interrelated processes.
A method for analyzing a composition of interacting services in a distributed system, comprising:
- generating a concurrent process graph (CPG) for processes in a system;
- symbolically encoding the CPG of each process to perform a reachability analysis;
- generating symbolic summaries for concurrently running processes based on the reachability analysis;
- and
- utilizing the symbolic summaries of the processes to analyze a system of interrelated processes.
A system for verification of services in a distributed system, comprising:
- a concurrent process graph (CPG) generated for the plurality of processes in a distributed system;
- a symbolic encoder configured to symbolically encode the CPG of each process to perform a reachability analysis;
- a library of process summaries stored in a memory media, the process summaries representing concurrently running threads and processes based on reachable states;
- and
- a modular verifier configured to perform service composition by computing and utilizing the process summaries of the processes to modularly analyze an entire system of processes to determine dependencies and order of execution for the entire system of process.
Dependencies are inferred from the claim text.