Applying Multilayer Modeling and Verification to All-Optical Computer Networks

• Název v anglickém jazyce: Applying Multilayer Modeling and Verification to All-Optical Computer Networks
• Akademický rok vypsání: 2013/2014
• Typ práce: disertační práce
• Jazyk práce: angličtina
• Ústav: Katedra distribuovaných a spolehlivých systémů (32-KDSS)
• Vedoucí / školitel: doc. RNDr. Jan Kofroň, Ph.D.
• Řešitel: skrytý - zadáno a potvrzeno stud. odd.
• Datum přihlášení: 27.09.2013
• Datum zadání: 27.09.2013
• Datum potvrzení stud. oddělením: 27.01.2014

Zásady pro vypracování

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.

Seznam odborné literatury

[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.