1 Introduction

In the vision of Ambient Intelligence, technology becomes invisible, embedded in our natural surroundings, present whenever we need it, enabled by simple and effortless interactions, attuned to all our senses, adaptive to users and context and autonomously acting  [1]. Interactive media presentations will no longer be folded in a flat screen with 5.1 speakers, but instead, will be distributed into the user’s environment. The environment with distributed and networked interfaces, functioning as interactive theater, will engage people in more immersive experiences. In a previous study done in Philips Electronics, we have shown how to structure the content and system to present interactive media to a distributed environment that consists of not only screens and speakers, but also lights and robots  [7, 6]. It was done in the context of EU funded R&D projects (NexTV  [11] and ICE-CREAM  [9]). (Figure 1 shows two users interacting with the ICE-CREAM demonstration, exhibited in IBC 2003  [8]).

---

---

One of the problems is the variety of such environments - thinking of how different people arrange their living rooms. This has been a long-existing problem with regard to web browsers. In order to give the same look-and-feel on a single web page to the users, the poor authors often have to work very hard to use all kinds of tricks, and when this fails, write different versions for different browsers. On the other hand, web authors are lucky - if they only consider Internet Explorer, they will possibly cover 4/5 of the audience, and if they are kind enough to consider Mozilla users, they will almost cover them all. We are not that lucky. We can not assume that there are only Explorer-like living rooms and Mozilla-like living rooms. They are different, in terms of available components and connections. It is impossible to have one version to fit them all. Instead we should have only one abstract media description for all living rooms, then map the media needs to every physical room, to create the experience for end users as intended as possible. Similar mapping problems are studied informally in  [10].

We aim at the formalization of such mapping problems. Each mapping problem is defined by a set of media needs and a set of presentation resources. The media needs are abstract description of the media content as well as its requirements for the physical components and their connections, including for example audiovisual players, robotic interactors and lights. These physical components are presentation resources. We employ Broy’s stream-based component framework  [2]. The following issues must be addressed:

1.

component interfaces for control and for events;

2.

user interfaces: touch screens, switches and buttons;

3.

throughput requirements and network delays;

4.

embedding of presentation components into devices;

5.

standardization of specifications (keeping the math away from the media developers).

The formalization will serve as a helpful framework for the development of an automated mapper that can handle real media needs and real presentation resources.

The mapping is to find the presentation resources for a set of media so that each media content is properly presented. In a typical implementation a mapping is a process that at run-time deals with control and events, and that has access to a number of reserved presentation resources. A presentation could be built by a “mapping server”, which behaves as a factory  [3], launching presentations. Of course the mapping server takes a mapping problem (= media needs + presentation resources) as its input, solves the mapping problem, makes the reservations, and then builds and launches the presentation. In fact, a presentation could be structured as a main process by the mapper server, upwards serving the media needs, and several distributed and auxiliary processes downwards employing the local resources from the devices in the environment. Typically, a distributed presentation is built by a local server (also a factory). Although one may expect that one such server per device would be sufficient, this is actually not the case; the reason is that several mutually incompatible software abstractions exist upon the the same device (for example, the Real player and the Microsoft media player on a Windows PC).

2 Preliminaries

To get started we consider a few simple media needs:

• high-resolution video presentation
• low-resolution video presentation
• dancing behavior
• up-down interactor

which have to be obtained from the following resources:

• cable: upc cable 801(10Mb/s)
• the__sign: www.clips.com/the__sign.mpg (10Kb/s)
• happy__puppy: www.dance.com/happy__puppy.dhb (1Kb/s)
• updown: /interactors/updown.exe (1b/s).

To model the media needs and presentation resources, we follow the approach of Broy  [2] based on timed streams. We have some drawing conventions of our own, which is derived from ADL Darwin  [5, 4]. We use
instead of (See  [2], p.7).

In an interactive presentation system, it is necessary to distinguish user interface channels from data streaming channels. For this we add another convention, namely output channels ■ modeling real, physical presentations such as sounds, video frames and robotic movements, and input channels □ modeling the components with which the user may interact with the system, such as a GUI interface on a screen and physical buttons on a remote control.

Broy demands that a set S of types be given. We put

for PAL streams, MPEG streams, Dancing BeHavior, Interaction BeHavior and “things in the ℝeal world”(for example, buttons, screens and robots).

In Broy’s approach there is a discrete time frame representing time as an infinite chain of time intervals of equal finite duration. We take 1 second for that duration. This allows us to formally represent the facts for example that there are 25 video frames per second in a high-resolution video stream and that each frame takes a number of bits.

We assume functions on data:

and obtain lifted versions of pr at timed-stream level: and so on. The formal model has some structure of its own (Figure 2).

---

---

In order to map this we must assume devices and connections. Figure 3 shows a possible configuration with the following devices:

• STB: set-top box;
• modem: internet modem;
• hi__res&PIP: high-resolution monitor with picture-in-picture function;
• lo__res: low-resolution (lo__res) monitor;
• level2_robot: “level-2” robot;
• RC: remote control for the low-resolution monitor

and the following connections:

• STB - modem 100b/s duplex;
• STB - hi__res 100Mb/s duplex;
• modem - lo__res 1Mb/s duplex;
• modem - robot 10Kb/s duplex;
• RC - lo__res 100b/s duplex.

---

---

There are two possible ways of presenting the dancing behavior: either by an animated character on the PIP of the hi__res screen, or by the physical robot together with the RC providing user input. But the STB - modem bandwidth is not enough for the PIP to do it. So the robot must dance and the RC must provide the up-down interaction.

3 Specification

We need some abbreviations. For timed stream z and n₁, n₂ ∈ ℕ,

with the intuition that e.g. rate(z,100,100K) means that 100 frames fit into once second and that 100K bits go into each frame (Figure 4).

---

---

For timed streams x and x′, and Δ ∈ ℕ,

and for m ∈ ℕ,

The rate information is put into the source devices S₁, S₂, S₃ and the sink S₄.

The relation between media formats and the real world is described in P₁,..., P₄.

Matters of delay are modelled in the channels.

Finally the whole system is specified by:

which has a syntactic interface of (I, O), where

4 Presentation resources

The next step is to formalize the presentation resources, i.e. the components and the network connections. We assume that the components cause delays and that the connections give rise to bandwidth restrictions. The structure of the resulting model is shown in Figure 5. Clearly we will need renaming later, for example, [the__sign∕url₁] (for modem) and [cable∕channel] (for STB).

---

---

Somehow the components must be configured to perform the required routing of streams. Although the current mapping-example does not require it, in general a component must be able to combine two incoming streams and put them on a single output port, or conversely, split what comes in to produce separate outgoing streams. In other words, some components must contain a switch.

A component containing a switch must have an extra channel of a special type, a control channel, accepting so-called commands, from a set ℂ. So from now on,

To get some experience in modelling switches, we try a simplified component, the Simple Switch SS:

Any selection from x, y and z can be combined and offered on u, provided the rates fit. To adapt to the rate of u, which is assumed to be fixed, dummy data must be stuffed.

We assume the existence of disjoint copies of the set DBH, which we denote DBH₁, DBH₂, etc. We also assume conversion functions d₁ : DBH → DBH₁, d₂ : DBH → DBH₂, etc. and the corresponding inverses, e.g. d₁^-1 : DBH₁ → DBH. They give rise to lifted versions, e.g. d₁′ : DBH^*→ DBH₁^*. These assumptions allow us to specify streams being merged, e.g. x and y merged into u:

In other words, the mechanism of disjoint copies is used to model tagging of sub-streams conveniently in an abstract way. (In Broy’s theory, means the stream obtained from x by deleting all its messages that are not elements of the set S.)

We introduce abbreviations:

Although a real network connection carries bits, we use a more abstract model to reflect the general-purpose nature of connections:

where DBH₀ ≜ DBH (So this can be used for the simple case where tagging is not really needed).

On the basis of this example, we consider the real components, assuming the real delay occurs in the components as show in the following table. This means that a constraint such as delay(x, u,Δ_SS) has to be rewritten as . We assume that the delay is fixed, independent of the load and the precise routing. Otherwise, more sophisticated schemes can be devised if necessary. Note that is the lifted version of . The rate constraints are modelled as if they belong to the input ports.

5 Mapping

Next we propose a mapping. Abstractly, a mapping is a set of paths through a given network, one path for each of the four chains specified in SYSTEM. At a concrete level, the paths are established by feeding appropriate switching commands into STB, modem and lo__res. In general there is a freedom in choosing these paths, for example if alternative routing through the network exists. Even the choice of which screen or interactive input is to be used is not a priori fixed. The four paths are shown in Figure 6. In an informal way it is easy to check that the delay and bandwidth constraints are not violated and the mapping is feasible.

---

---

To formalize the connections we use renaming by adapting port names to “wire names”. The wire names are also shown in Figure 6. Note that w4a, w4b and w4c together form a path from RC via lo__res and modem to STB. The other wire names are not used. Unused ports must be hidden and ports that go to the external world must be renamed.

Finally the whole system implementation is described by

which has the syntactic interface (I′, O′), where

6 Correctness

The next questions is: how to express the formal correctness of the implementation?

Broy proposes three ideas of refinement: property refinement, glass box refinement, and interaction refinement. The glass box refinement is a classical concept of refinement typically used to decompose a system with a specified black box behavior into a distributed system architecture in the design phase, which seems appropriate in our case. The general form of a glass box refinement is

(In Broy’s theory (see  [2]), there is also another form for state machines, which we don’t need here). The relation ⊆ on component behaviors is defined by the rule that ⊆ F stands for the proposition where

Also recall the definition of ⊕ for F₁ ⊕ F₂

Let RATE′ be given by

Note that this is essentially the same as S₁,..., S₄ are saying about their z ports.

Consider an arbitrary x satisfying RATE′ where where I′ is {cable,...}. x is a channel valuation x : I′→ (M^*)^∞ such that

where M = ⋃ _s∈Ss = PAL ∪ MPG ∪ DBH ∪ IBH ∪ ℝ

Since I′ has only four elements, we can write this out by assuming

Now this x satisfies RATE′, that is, x_u has 100 frames per second, each frame being 100K bits, etc. (And similarly, x_d: 10, 100 respectively, x_c: 2, 5K respectively and x_b: 1, 1 respectively.)

Let y ∈ SYSTEM′.x where where O′ is {screen, screen′, moving, updown} which we write out by assuming

The correctness requirement is

because SYSTEM′ only specifies maximal rates where as SYSTEM has already fixed the rates.

The obvious proof strategy is to take an arbitrary x satisfying RATE′ and consider a y ∈ SYSTEM′.x, i.e.

and then check that y ∈ SYSTEM.x, which essentially boils down to checking maxdelay constraints and checking the essential transformations of the form pr′′ for each of the specification paths, e.g. when going from cable to screen, or when going from the__sign to screen′.

As an example we check that y_s satisfies all constraints of SYSTEM.x. Since SYSTEM falls apart in 4 unconnected parts, it is enough to check that y_s = y.screen satisfies the the constraints of (S₁ ∘ C₁ ∘ P₁)\{z, w}:

which is equivalent to: (since pr′′ works frame-wise.)

What we know about y_s comes from RATE′∧ SYSTEM′ which for RATE′ means rate(cable,100,100K). For SYSTEM′, its meaning is more complicated. First, note that

also, SYSTEM′ = (STB′⊕ hi__res&PIP′⊕), where

Note that for y_s it suffices to focus on STB′ and hi__res&PIP and forget about all other channels than w₁ where ⊕ can be replaced by ∘, i.e.

We summarize the assertions from SYSTEM′ by performing the renamings and keeping only the relevant clauses in view of the chosen control command. STB′ says:

hi__res&PIP′ says from rate(x.cable,100,100K) we decide that for all t and for each i, the i-th frame has therefore so the maxrate requirement of STB′ saying is not contradicted.

Next we check the delays. We combine the two one-step delay assertions, first by noting that pr′′ works frame-wise:

and secondly by adding the delays: which satisfies the clause from SYSTEM that as required. The other SYSTEM constraints can be checked in a similar manner.

7 Concluding remarks

The case study shows how Broy’s framework can deal with special interfaces for control and events at an abstract level and with real-world interfaces. It can also deal with bandwidth requirements and network delays very well. The case study does not have a sophisticated performance model, but it is plausible that certain models can be made using the same modelling style (for example if the delay is a function of the bit rate).

The case study shows one specification and one configuration of presentation resources. Abstractly, the mapping between the two is a set of paths through the network. Concretely, a mapping is a set of control commands, to be given to those components that have switching capabilities. Maximal rate and delay requirements can be checked formally, although the calculations are not surprising. Media types are described by sets such as PAL and MPG, this implies that type compatibilities are handled formally too.

The model created focuses on the stream-based aspects; in this type of distributed systems these aspects are most important at the architectural level. At a protocol level, we expect that reactive behavior is most important, and complementary state-machine based models could be used  [12].

The following research questions remain as options for future research:

1.

How to model dynamic aspects such as changing configurations and servers that build presentations according to the “factory” paradigm;

2.

How to scale-up the approach when more and more technicalities have to be modelled (while keeping the math away from media developers);

3.

How to specify the general class of “mapping problems” (instead of a single instance, as we did now).

Acknowledgement

The authors would like to thank Emile Aarts and Maddy Janse from Philips Research Eindhoven for their support on the work and Yuechen Qian for his comments on the early draft of this paper.

References