Name
Abstract | ||
|---|---|---|
Model checking has been widely used in program verification and debugging. In this paper, we present ModelX, which makes the first step towards using formal methods to verify the design of large-scale cloud applications. Our basic idea is to model the high-level behavior of cloud applications in early design, and use the distributed model checker, SPIN, to verify whether the LTL (linear temporal logic) is satisfied. We apply the idea to 4 known failed system designs, two from Microsoft, one from Facebook, and one from Amazon, to replay the failures, which demonstrate the feasibility of our proposals. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/CIT.2016.66 | 2016 IEEE International Conference on Computer and Information Technology (CIT) |
Keywords | Field | DocType |
model checking,cloud applications,design errors detection | Structured systems analysis and design method,Distributed element model,Programming language,Model checking,Computer science,Server,Real-time computing,Linear temporal logic,Formal methods,Distributed computing,Cloud computing,Debugging | Conference |
ISBN | Citations | PageRank |
978-1-5090-4315-6 | 0 | 0.34 |
References | Authors | |
3 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tian Tian | 1 | 86 | 18.09 |
| Yiming Zhang | 2 | 143 | 37.82 |
| Qiao Zhou | 3 | 0 | 1.01 |
| Ping Zhong | 4 | 40 | 11.34 |