Applying Multilayer Modeling and Verification to All-Optical Computer Networks

• Thesis title in English: Applying Multilayer Modeling and Verification to All-Optical Computer Networks
• Academic year of topic announcement: 2013/2014
• Thesis type: dissertation
• Thesis language: angličtina
• Department: Department of Distributed and Dependable Systems (32-KDSS)
• Supervisor: doc. RNDr. Jan Kofroň, Ph.D.
• Author: hidden - assigned and confirmed by the Study Dept.
• Date of registration: 27.09.2013
• Date of assignment: 27.09.2013
• Confirmed by Study dept. on: 27.01.2014

Guidelines

All-optical communication networks and their properties are not yet well understood on the formal level. No modeling scheme descriptive enough to comprise all of their substantial properties is currently available. However, turning a network into a formal model enables a wide area of possibilities towards machine reasoning and design validation. The aim of this thesis is to significantly advance the state of the art in computer network modeling and property verification.

References

[1] Baier, C. and Katoen, J.-P.: Principles of Model Checking. MIT Press 2008.
[2] Dijkstra, F.: Framework for Path Finding in Multi-Layer Transport Networks. UoA 2009.
[3] McMillan, K. L.:. Symbolic Model Checking. Kluwer Academic 1993.
[4] Clarke, E. M. and Grumberg, O. and Peled, D.: Model Checking. MIT Press 1999.
[5] Guerraoui, R. and Yabandeh, M.: Model Checking a Networked System Without the Network. School of Computer and Communication Sciences, EPFL 2011.
[6] Musuvathi, M.: CMC: A Model Checker for Network Protocol Implementations. Stanford University 2004.
[7] Beckman, N. E. and Nori, A. V. and Rajamani S. K. and Simmons, R. J.: Proofs from tests. ISSTA'08, ACM 2008.
[8] Stahl, T. and Voelter, M.: Model-Driven Software Development: Technology, Engineering, Management. Wiley 2006.
[9] Hallal, H. and Petrenko, A. and Boroday, S.: A Model Checking Approach to Network Fault Management. SCI AND ISAS, 2011.