Formal modelling for digital media distribution

Human beings have always strived to preserve their memories and spread their ideas. In the beginning this was always done through human interpretations, such as telling stories and creating sculptures. Later, technological progress made it possible to create a recording of a phenomenon; first as an analogue recording onto a physical object, and later digitally, as a sequence of bits to be interpreted by a computer. By the end of the 20th century technological advances had made it feasible to distribute media content over a computer network instead of on physical objects, thus enabling the concept of digital media distribution. Many digital media distribution systems already exist, and their continued, and in many cases increasing, usage is an indicator for the high interest in their future enhancements and enriching. By looking at these digital media distribution systems, we have identified three main areas of possible improvement: network structure and coordination, transport of content over the network, and the encoding used for the content. In this thesis, our aim is to show that improvements in performance, efficiency and availability can be done in conjunction with improvements in software quality and reliability through the use of formal methods: mathematical approaches to reasoning about software so that we can prove its correctness, together with the desirable properties. We envision a complete media distribution system based on a distributed architecture, such as peer-to-peer networking, in which different parts of the system have been formally modelled and verified. Starting with the network itself, we show how it can be formally constructed and modularised in the Event-B formalism, such that we can separate the modelling of one node from the modelling of the network itself. We also show how the piece selection algorithm in the BitTorrent peer-to-peer transfer protocol can be adapted for on-demand media streaming, and how this can be modelled in Event-B. Furthermore, we show how modelling one peer in Event-B can give results similar to simulating an entire network of peers. Going further, we introduce a formal specification language for content transfer algorithms, and show that having such a language can make these algorithms easier to understand. We also show how generating Event-B code from this language can result in less complexity compared to creating the models from written specifications. We also consider the decoding part of a media distribution system by showing how video decoding can be done in parallel. This is based on formally defined dependencies between frames and blocks in a video sequence; we have shown that also this step can be performed in a way that is mathematically proven correct. Our modelling and proving in this thesis is, in its majority, tool-based. This provides a demonstration of the advance of formal methods as well as their increased reliability, and thus, advocates for their more wide-spread usage in the future.

Viologen based electroactive polymers and composites for durable electrochromic systems

Electrochromism, the phenomenon of reversible color change induced by a small electric charge, forms the basis for operation of several devices including mirrors, displays and smart windows. Although, the history of electrochromism dates back to the 19th century, only the last quarter of the 20th century has its considerable scientific and technological impact. The commercial applications of electrochromics (ECs) are rather limited, besides top selling EC anti-glare mirrors by Gentex Corporation and airplane windows by Boeing, which made a huge commercial success and exposed the potential of EC materials for future glass industry. It is evident from their patents that viologens (salts of 4,4ʹ-bipyridilium) were the major active EC component for most of these marketed devices, signifying the motivation of this thesis focusing on EC viologens. Among the family of electrochromes, viologens have been utilized in electrochromic devices (ECDs) for a while, due to its intensely colored radical cation formation induced by applying a small cathodic potential. Viologens can be synthesized as oligomer or in the polymeric form or as functionality to conjugated polymers. In this thesis, polyviologens (PVs) were synthesized starting from cyanopyridinium (CNP) based monomer precursors. Reductive coupling of cross-connected cyano groups yields viologen and polyviologen under successive electropolymerization using for example the cyclic voltammetry (CV) technique. For further development, a polyviologen-graphene composite system was fabricated, focusing at the stability of the PV electrochrome without sacrificing its excellent EC properties. High electrical conductivity, high surface area offered by graphene sheets together with its non-covalent interactions and synergism with PV significantly improved the electrochrome durability in the composite matrix. The work thereby continued in developing a CNP functionalized thiophene derivative and its copolymer for possible utilization of viologen in the copolymer blend. Furthermore, the viologen functionalized thiophene derivative was synthesized and electropolymerized in order to explore enhancement in the EC contrast and overall EC performance. The findings suggest that such electroactive viologen/polyviologen systems and their nanostructured composite films as well as viologen functionalized conjugated polymers, can be potentially applied as an active EC material in future ECDs aiming at durable device performances.

Standardized electrical tests for electrical equipment in road vehicles Case: Visedo Oy PowerMASTER M-frame

Electrical road vehicles were common at the begin of the 20th century but internal combustion engines took a victory from electrical motors in road vehicles. The acknowledgement of the environment, and the price and the availability of the crude oil are reasons for the comeback of the electrical vehicles. Advancement in industrial technology and political atmosphere in EU as the directive 20--20--20, which consists of reducing fossil emission, increasing renewable energy and increasing the energy efficiency, have made the electrification popular again. In this thesis tests based on standard ISO 16750--2 electrical loads for electrical equipment in road vehicles are made for Visedo Oy's PowerMASTER M-frame power electronics device. This device is designed for mainly drive trains in mobile work machines and marine vessels but can be used in other application in its power range which also includes road vehicles. The functionality of the device is tested with preliminary tests which act as a framework for the tests based on standards.