University of Twente Student Theses
Verifying functional requirements in multi-layer networks: a case for formal description of computer networks
Aertsen, M.Y. (2014) Verifying functional requirements in multi-layer networks: a case for formal description of computer networks.
This is the latest version of this item.
|
PDF
1MB | |
|
PDF
1MB |
| Abstract: | Major outages and hacks in corporate networks show that the mounting complexity in computer networks has a direct impact on business. Although users have an intuitive understanding of how they would like the network to behave, network operators lack tools to match these implicit requirements against actual infrastructure. Verification is in the stone-age, with visual tracing of diagrams and drawings being the most common method to check network topology for conformance with user expectations. It is both tiresome and error-prone and does not scale beyond SME networks. The main aim of this research is to examine the feasibility of automated property checking of real world networks. We build on work on network topology descriptions and multi-layer path selection and study the possibility of expressing expected behaviour on top of existing technology-independent algorithms, answering the question: "Is it possible to verify operational requirements in multi-layer networks via algorithms for path selection in their topology descriptions?" We have found that there are topology descriptions languages available that allow formal description of networks for the purpose of reasoning. We have shown that it is possible to formally define operational requirements using a graph definition obtained from such descriptions. Using this formal definition we have synthesised verification algorithms to test conformance to such a requirement. These algorithms have been deomonstrated to decompose in multi-layer path selection and verification. And finally, we have shown a working proof of concept which puts these ideas in practice in a real world network. Our conclusion: it is possible to verify operational requirements in multi-layer networks via algorithms for path selection in their topology descriptions. |
| Item Type: | Essay (Master) |
| Clients: | Deloitte, Nederland |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Internet Science and Technology MSc (60032) |
| Link to this item: | https://purl.utwente.nl/essays/64707 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page