Name
Abstract | ||
|---|---|---|
Next generation cyber-physical systems (CPS) are expected to be deployed in domains which require scalability as well as performance under dynamic conditions. This scale and dynamicity will require that CPS communication networks be programmatic (i.e., not requiring manual intervention at any stage), but still maintain iron-clad safety guarantees. Software-defined networking standards like Openflow provide a means for scalably building tailor-made network architectures, but there is no guarantee that these systems are safe, correct, or secure. In this work we propose a methodology and accompanying tools for specifying and modeling distributed systems such that existing formal verification techniques can be transparently used to analyze critical requirements and properties prior to system implementation. We demonstrate this methodology by iteratively modeling and verifying an Openflow learning switch network with respect to network correctness, network convergence, and mobility-related properties. We posit that a design strategy based on the complementary pairing of software-defined networking and formal verification would enable the CPS community to build next-generation systems without sacrificing the safety and reliability that these systems must deliver. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2461446.2461461 | HiCoNS |
Keywords | Field | DocType |
tailor-made network architecture,network correctness,verifiably-safe software-defined network,software-defined networking standard,switch network,formal verification technique,cps communication network,cps community,network convergence,software-defined network,formal verification,openflow,software defined networks | Computer science,Correctness,Network architecture,Real-time computing,Network switch,OpenFlow,Cyber-physical system,Software-defined networking,Formal verification,Scalability,Distributed computing | Conference |
Citations | PageRank | References |
16 | 0.89 | 11 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Richard William Skowyra | 1 | 29 | 2.19 |
| Andrei Lapets | 2 | 75 | 10.53 |
| Azer Bestavros | 3 | 3791 | 764.82 |
| Assaf Kfoury | 4 | 33 | 3.87 |