LAP LAMBERT Academic Publishing, 2013.- 292 p. ISBN 978-3-659-42228-7Foundations of the functional Petri net theory were developed for the analysis of
detailed models of networking protocols. Methods of timed Petri nets reduction on the
basis of equivalent transformations of formulas describing their transfer function were
constructed; weak types of nets equivalence were investigated. Methods of synthesis of
continuous (fuzzy) logic functions given in tabular form were developed. Bases of the
theory of clans of systems of the linear algebraic equations were built, allowing the
acceleration of the systems solving in rings with a sign, as well as the corresponding
algorithms and software. Methods of synthesis of Petri net models on standard
specifications of telecommunication protocols with use of intermediate language of co-
operating consecutive Hoare processes were developed. Petri net model of the electronic
commerce protocol IOTP was synthesized. Verification of protocols ECMA, BGP,
TCP, IOTP was fulfilled. The method of compositional calculation of invariants for
infinite Petri nets with regular structure was developed; the method was applied for the
proof of invariance of Petri net model of Ethernet network with the common bus
topology. Methods of construction of models of telecommunication systems by a
composition of models of components and estimations of functional characteristics of
models were developed; switched Ethernet, label switching network MPLS and wireless
network Bluetooth were investigated.Table of contents:Tasks of processes modeling in telecommunication systems and networks.
Verification of networking protocols.
Estimation of efficiency of telecommunication systems and networks.
Simulation modeling of telecommunication systems.
Modeling telecommunication systems by Petri nets.
Verification of protocols by means of Petri net models.
Colored Petri nets as means of simulation modeling of telecommunication systems.
Decomposition and reduction of Petri nets.
Solution of systems of linear Diophantine equations.Functional Petri nets.
Basic concepts and definitions.
Properties of functional subnets.
Methods of Petri net decomposition into functional subnets.
Transfer function of Petri net.
Synthesis of continuous logic functions given in tabular form.
Efficient implementation of algorithm of decomposition into functional subnets.Clans of systems of linear algebraic equations.
Algebraic methods of Petri nets analysis.
Clans of linear systems as a generalization of functional Petri nets.
Composition of clans of linear systems.
Sequential composition of clans of linear systems.
Optimal collapse of a weighted graph.
Algorithms of compositional solution of systems of linear algebraic equations.Synthesis of Petri net models and verification of networking protocols.
Petri net as a uniform language of protocols specification.
Building Petri net model of protocol BGP.
Building Petri net model of protocol TCP.
Verification of protocol BGP.
Verification of protocol TCP.
Methods of synthesis of Petri net models of protocols.
Synthesis of Petri net model and verification of the electronic commerce protocol IOTP.
Verification of protocols with unlimited number of interacting devices.
Protocols of Ethernet with architecture of the common bus.
Model of Ethernet with architecture of the common bus.
Calculation of invariants in the parametric form.Performance evaluation of networks by colored Petri nets.
Models of switched Ethernet networks.
Model of a local area network.
Model of switch.
Models of workstation and server.
Parameters of the model.
Method of measuring fragments.
Models of networks with labels switching MPLS.
Overview of labels switching technology MPLS.
Model of IP router.
Model of MPLS router.
Model of the European Internet backbone.
Models of terminal networks.
Comparative estimation of IP routing and MPLS.
Models of Bluetooth networks.
Bluetooth technology overview.
Model of slave device.
Model of master device.
Models of piconets.
Estimation of efficiency of address space usage.
Measurement of characteristics of real-life networks.Verification of protocol ECMA.
Theoretical justification and estimations of complexity of Toudic method.
Tracing frames’ passage within the model of switched Ethernet.
