As already presented, the Internet routing system is partitioned into tens of thousands of independently administered Autonomous Systems (ASs). The Border Gateway Protocol (BGP) is the de facto inter-domain routing protocol that maintains and exchanges routing information between ASs. However, the BGP was designed based on the implicit trust between all participants and does not employ any measure to authenticate the routes injected into or propagated through the system. Therefore, virtually any AS can announce any route into the routing system, and sometimes the bogus routes can trigger large-scale anomalies in the Internet. A canonical example occurred on April 25, 1997, when a misconfigured router maintained by a small service provider (AS7007) in Virginia, USA, injected incorrect routing information into the global Internet and claimed to have optimal connectivity to all Internet destinations. As a result, most Internet traffic was routed to this small ISP. The traffic overwhelmed the misconfigured and intermediate routers, and effectively crippled the Internet for almost two hours. Since then, many such events have been reported, some of them due to human mistakes, others due to malicious activities that exploited vulnerabilities in the BGP in order to cause large-scale damage. For example, it is common for spammers to announce an arbitrary prefix and then use that prefix to send spam from the hijacked address space, making the trace back and the spammer identity discovery much more difficult.

Since the 1950s, voice and video services such as telephony and television have established themselves as an integral part of everyone's life. Traditionally, voice and video service providers built their own networks to deliver these services to customers. However, tremendous technical advancements since the 1990s have revolutionized the mode of delivery of these services. Today, these services are delivered to the users over the Internet, and we believe that there are two main reasons for this: (i) delivering services over the Internet in IP packets is much more economical for voice and video service providers and (ii) the massive penetration of broadband (i.e. higher bandwidth) Internet service has ensured that the quality of voice and video services over the Internet is good enough for everyday use. The feasibility of a more economical alternative for voice and video services attracted many ISPs including Comcast, AT&T and Verizon, among several others, to offer these services to end users at a lower cost. However, non-ISPs, such as Skype, Google, Microsoft, etc. have also started offering these services to customers at extremely competitive prices (and, on many occasions, for free).

From an ISP's perspective, traffic classification has always been a critical activity for several important management tasks, such as traffic engineering, network planning and provisioning, security, billing and Quality of Service (QoS). Given the popularity of voice and video services over the Internet, it has now become all the more important for ISPs to identify voice and video traffic from other service providers for three reasons.

Since the late 1990s there has been significant interest and attention from the research community devoted to understanding the key drivers of how ISP networks are designed, built and operated. While recent work by empiricists and theoreticians has emphasized certain statistical and mathematical properties of network structures and their behaviors, this part of the book presents in great detail an optimization-based perspective that focuses on the objectives, constraints and other drivers of engineering design that will help the community gain a better insight into this fascinating world and enable the design of more “realistic” models.

In this chapter we introduce the area of IP network design and the factors commonly used to drive such a process. Our discussion revolves around IP-over-WDM networks, and we define the network design problem as the end-to-end process aimed at identifying the “right” IP topology, the associated routing strategy and its mapping over the physical infrastructure in order to guarantee the efficient utilization of network resources, a high degree of resilience to failures and the satisfaction of SLAs.

We start by providing a high-level overview of the IP-over-WDM technology. We highlight the properties of the physical and IP layers (the IP layer is also known as the logical layer), we discuss their relationship, and introduce the terminology that will be extensively used in the following chapters. Then, we introduce the processes encountered in IP network design and their driving factors.

Due to the challenges of obtaining an AS topology annotated with AS relationships, it is infeasible to use the valley-free rule to identify redistribution path spoofing in the work. Alternatively, we apply the direction-conforming rule to the AS topology annotated with directed AS-links to carry out the detection. The following theorems show that the direction-conforming rule actually shows roughly equivalent efficiency.

Theorem D.1

For an observer AS, a valley-free path in the AS topology annotated with AS relationships must be “direction-conforming” in the corresponding AS topology annotated with inferred directed AS-links.

Theorem D.2

1. (1) For a Tier-1 AS, the direction-conforming paths in the AS topology annotated with inferred directed AS-links must be valley-free in the real AS topology annotated with AS relationships.

2. (2) For a non-Tier-1 AS, except the redistribution path-spoofing paths launched by the provider ASs, the direction-conforming paths must be valley-free.

In order to prove these theorems, we first investigate the mapping between the real AS topology annotated with AS relationships and the inferred AS topology annotated with directed AS-links.

Note that, similar to the analysis in the text, we assume that the inferred topology is “ideally” complete, namely it contains all legitimate directed AS-links that the observer AS should see. In order to infer a complete AS topology comprising of directed AS-links based on the route announcements from the observer AS, we assume an ideal inference scenario, in which the AS connections and relationships do not change over the inference period and every AS tries all possible valid routes.

In industrial automation the aim is to control and optimise production processes and to provide high-quality and reliable products and services by minimising material, cost, and energy waste. Automation systems rely on smart sensors, actuators, and other industrial equipment like robotic and mechatronic components. Open and standardised communication networks are employed for the communication as well as configuration and control of the various automation components. The standard architecture consists of PLCs (Programmable Logic Controllers) or DCS (Distributed Control Systems), fieldbus systems, and PCs serving as man/machine interfaces as well as intelligent sensors and actuators (e.g. frequency converters). The fieldbus systems gather the signals from the process level or the sensors and actuators with fieldbus interfaces, and are directly connected to distributed or centralised control devices, such as PLCs.

The standard IEC 61131-3 of the International Electrotechnical Commission provides a range of programming notations suitable for implementation on PLCs. It comprises basic notations close to those in electrical engineering like contact plans, instruction lists, and function plans as well as graphical and textual programming notations called sequential function charts and structured text. Currently, the development of software in automation technology proceeds step by step along the life cycle using the notations of this standard and different tools provided by different PLC vendors.

A problem is that different PLC vendors use their own variants of the standard with different syntax, semantics, and tool sets. Also, the approaches based on the standard are not well suited for the development of distributed applications and applications with hard real-time requirements.

The Duration Calculus can be used as a high-level specification language for properties of real-time systems. The question arises whether reasoning about such specifications can be automated. To this end, we first discuss the decidability of the realisability problem of the Duration Calculus: is there an algorithm that for a given Duration Calculus formula decides whether this formula can be realised. By using proof techniques of Zhou Chaochen, M.R. Hansen, and P. Sestoft, we show that for a subset of the Duration Calculus and the discrete-time domain this problem is indeed decidable. However, for the general case of continuous time it is not. The proofs of these results shed light on the difference between these two time domains.

Next we introduce the subset of implementables due to A.P. Ravn. This subset provides certain patterns of formulas formalising concepts like stability and progress that are convenient for specifying the behaviour of controllers. Finally, we introduce Constraint Diagrams due to C. Kleuker as a graphical representation of a subset of Duration Calculus. These diagrams specify timed behaviours in an assumption/commitment style. We show that the implementables all have lucid representations as Constraint Diagrams. In general, Constraint Diagrams are more expressive than implementables.

Decidability results

Zhou Chaochen, M.R. Hansen, and P. Sestoft showed that the problem whether a given DC formula is satisfiable is decidable for a subset of DC when discrete time is assumed [ZHS93]. This result has been exploited by P.K. Pandya in a tool called DCVALID for automatically checking satisfiability and validity of formulas in this subset [Pan01].

Computers are used more and more to provide high-quality and reliable products and services, and to control and optimise production processes. Such computers are often embedded into the products and thus hidden to the human user. Examples are computer-controlled washing machines or gas burners, electronic control units in cars needed for operating airbags and braking systems, signalling systems for high-speed trains, or robots and automatic transport vehicles in industrial production lines.

In these systems the computer continuously interacts with a physical environment or plant. Such systems are thus called reactive systems. Moreover, common to all these applications is that the computer reactions should obey certain timing constraints. For example, an airbag has to unfold within milliseconds, not too early and not too late. Reactive systems with such constraints are called real-time systems. They often appear in safety-critical applications where a malfunction of the controller will cause damage and risk the lives of people. This is immediately clear for all applications in the transport sector where computers control cars, trains and planes.

Therefore the design of real-time systems requires a high degree of precision. Here formal methods based on mathematical models of the system under design are helpful. They allow the designer to specify the system at different levels of abstraction and to formally verify the consistency of these specifications before implementing them. In recent years significant advances have been made in the maturity of formal methods that can be applied to real-time systems.

Structure of this book

In this advanced textbook we shall present three such formal approaches:

• Duration Calculus (DC for short), a logic and calculus for specifying highlevel requirements of real-time systems;

• […]