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.

Production Quality Analysis of Special Elevator Cars Based on Six Sigma Approach

Project scope is to utilize Six Sigma DMAIC approach and lean principles to improve production quality of the case company. Six Sigma tools and techniques are explored through a literature review and later used in the quality control phase. The focus is set on the Pareto analysis to demonstrate the most evident development areas in the production. Materials that are not delivered to the customer or materials that damaged during transportation comprise the biggest share of all feedbacks. The goal is set to reduce these feedbacks by 50 %. Production observation pointed out that not only material shortages but also over-production is a daily situation. As a result, an initial picking list where the purchased and own production components can be seen, is created, reduction of over- and underproduction and material marking improvement are seen the most competitive options so that the goal can be reached. The picking list development should still continue to make sure that the list can be used not only in the case study but also in the industrial scale. The reduction of material missing category can be evaluated reliably not sooner than in few years because it takes time to gather the needed statistical information.

Control of Bubbling Fluidized Bed Conditions

The objectives of this master’s thesis were to understand the importance of bubbling fluidized bed (BFB) conditions and to find out how digital image processing and acoustic emission technology can help in monitoring the bed quality. An acoustic emission (AE) measurement system and a bottom ash camera system were evaluated in acquiring information about the bed conditions. The theory part of the study describes the fundamentals of BFB boiler and evaluates the characteristics of bubbling bed. Causes and effects of bed material coarsening are explained. The ways and methods to monitor the behaviour of BFB are determined. The study introduces the operating principles of AE technology and digital image processing. The empirical part of the study describes an experimental arrangement and results of a case study at an industrial BFB boiler. Sand consumption of the boiler was reduced by optimization of bottom ash handling and sand feeding. Furthermore, data from the AE measurement system and the bottom ash camera system was collected. The feasibility of these two systems was evaluated. The particle size of bottom ash and the changes in particle size distribution were monitored during the test period. Neither of the systems evaluated was ready to serve in bed quality control accurately or fast enough. Particle size distributions according to the bottom ash camera did not correspond to the results of manual sieving. Comprehensive interpretation of the collected AE data requires much experience. Both technologies do have potential and with more research and development they may enable acquiring reliable and real-time information about the bed conditions. This information could help to maintain disturbance-free combustion process and to optimize bottom ash handling system.