Scheduling dynamic dataflow graphs with model checking

With the shift towards many-core computer architectures, dataflow programming has been proposed as one potential solution for producing software that scales to a varying number of processor cores. Programming for parallel architectures is considered difficult as the current popular programming languages are inherently sequential and introducing parallelism is typically up to the programmer. Dataflow, however, is inherently parallel, describing an application as a directed graph, where nodes represent calculations and edges represent a data dependency in form of a queue. These queues are the only allowed communication between the nodes, making the dependencies between the nodes explicit and thereby also the parallelism. Once a node have the su cient inputs available, the node can, independently of any other node, perform calculations, consume inputs, and produce outputs. Data ow models have existed for several decades and have become popular for describing signal processing applications as the graph representation is a very natural representation within this eld. Digital lters are typically described with boxes and arrows also in textbooks. Data ow is also becoming more interesting in other domains, and in principle, any application working on an information stream ts the dataflow paradigm. Such applications are, among others, network protocols, cryptography, and multimedia applications. As an example, the MPEG group standardized a dataflow language called RVC-CAL to be use within reconfigurable video coding. Describing a video coder as a data ow network instead of with conventional programming languages, makes the coder more readable as it describes how the video dataflows through the different coding tools. While dataflow provides an intuitive representation for many applications, it also introduces some new problems that need to be solved in order for data ow to be more widely used. The explicit parallelism of a dataflow program is descriptive and enables an improved utilization of available processing units, however, the independent nodes also implies that some kind of scheduling is required. The need for efficient scheduling becomes even more evident when the number of nodes is larger than the number of processing units and several nodes are running concurrently on one processor core. There exist several data ow models of computation, with different trade-offs between expressiveness and analyzability. These vary from rather restricted but statically schedulable, with minimal scheduling overhead, to dynamic where each ring requires a ring rule to evaluated. The model used in this work, namely RVC-CAL, is a very expressive language, and in the general case it requires dynamic scheduling, however, the strong encapsulation of dataflow nodes enables analysis and the scheduling overhead can be reduced by using quasi-static, or piecewise static, scheduling techniques. The scheduling problem is concerned with nding the few scheduling decisions that must be run-time, while most decisions are pre-calculated. The result is then an, as small as possible, set of static schedules that are dynamically scheduled. To identify these dynamic decisions and to find the concrete schedules, this thesis shows how quasi-static scheduling can be represented as a model checking problem. This involves identifying the relevant information to generate a minimal but complete model to be used for model checking. The model must describe everything that may affect scheduling of the application while omitting everything else in order to avoid state space explosion. This kind of simplification is necessary to make the state space analysis feasible. For the model checker to nd the actual schedules, a set of scheduling strategies are de ned which are able to produce quasi-static schedulers for a wide range of applications. The results of this work show that actor composition with quasi-static scheduling can be used to transform data ow programs to t many different computer architecture with different type and number of cores. This in turn, enables dataflow to provide a more platform independent representation as one application can be fitted to a specific processor architecture without changing the actual program representation. Instead, the program representation is in the context of design space exploration optimized by the development tools to fit the target platform. This work focuses on representing the dataflow scheduling problem as a model checking problem and is implemented as part of a compiler infrastructure. The thesis also presents experimental results as evidence of the usefulness of the approach.

A complete map of the southern continent

Nimeketiedot nimiönkehyksissä

A complete map of the southern continent

Nimeketiedot nimiönkehyksissä

Adaptive Markov chain Monte Carlo and Bayesian filtering for state space models

This thesis is concerned with the state and parameter estimation in state space models. The estimation of states and parameters is an important task when mathematical modeling is applied to many different application areas such as the global positioning systems, target tracking, navigation, brain imaging, spread of infectious diseases, biological processes, telecommunications, audio signal processing, stochastic optimal control, machine learning, and physical systems. In Bayesian settings, the estimation of states or parameters amounts to computation of the posterior probability density function. Except for a very restricted number of models, it is impossible to compute this density function in a closed form. Hence, we need approximation methods. A state estimation problem involves estimating the states (latent variables) that are not directly observed in the output of the system. In this thesis, we use the Kalman filter, extended Kalman filter, Gauss–Hermite filters, and particle filters to estimate the states based on available measurements. Among these filters, particle filters are numerical methods for approximating the filtering distributions of non-linear non-Gaussian state space models via Monte Carlo. The performance of a particle filter heavily depends on the chosen importance distribution. For instance, inappropriate choice of the importance distribution can lead to the failure of convergence of the particle filter algorithm. In this thesis, we analyze the theoretical Lᵖ particle filter convergence with general importance distributions, where p ≥2 is an integer. A parameter estimation problem is considered with inferring the model parameters from measurements. For high-dimensional complex models, estimation of parameters can be done by Markov chain Monte Carlo (MCMC) methods. In its operation, the MCMC method requires the unnormalized posterior distribution of the parameters and a proposal distribution. In this thesis, we show how the posterior density function of the parameters of a state space model can be computed by filtering based methods, where the states are integrated out. This type of computation is then applied to estimate parameters of stochastic differential equations. Furthermore, we compute the partial derivatives of the log-posterior density function and use the hybrid Monte Carlo and scaled conjugate gradient methods to infer the parameters of stochastic differential equations. The computational efficiency of MCMC methods is highly depend on the chosen proposal distribution. A commonly used proposal distribution is Gaussian. In this kind of proposal, the covariance matrix must be well tuned. To tune it, adaptive MCMC methods can be used. In this thesis, we propose a new way of updating the covariance matrix using the variational Bayesian adaptive Kalman filter algorithm.

Remote sensing for three-dimensional modelling of hydromorphology

Successful management of rivers requires an understanding of the fluvial processes that govern them. This, in turn cannot be achieved without a means of quantifying their geomorphology and hydrology and the spatio-temporal interactions between them, that is, their hydromorphology. For a long time, it has been laborious and time-consuming to measure river topography, especially in the submerged part of the channel. The measurement of the flow field has been challenging as well, and hence, such measurements have long been sparse in natural environments. Technological advancements in the field of remote sensing in the recent years have opened up new possibilities for capturing synoptic information on river environments. This thesis presents new developments in fluvial remote sensing of both topography and water flow. A set of close-range remote sensing methods is employed to eventually construct a high-resolution unified empirical hydromorphological model, that is, river channel and floodplain topography and three-dimensional areal flow field. Empirical as well as hydraulic theory-based optical remote sensing methods are tested and evaluated using normal colour aerial photographs and sonar calibration and reference measurements on a rocky-bed sub-Arctic river. The empirical optical bathymetry model is developed further by the introduction of a deep-water radiance parameter estimation algorithm that extends the field of application of the model to shallow streams. The effect of this parameter on the model is also assessed in a study of a sandy-bed sub-Arctic river using close-range high-resolution aerial photography, presenting one of the first examples of fluvial bathymetry modelling from unmanned aerial vehicles (UAV). Further close-range remote sensing methods are added to complete the topography integrating the river bed with the floodplain to create a seamless high-resolution topography. Boat- cart- and backpack-based mobile laser scanning (MLS) are used to measure the topography of the dry part of the channel at a high resolution and accuracy. Multitemporal MLS is evaluated along with UAV-based photogrammetry against terrestrial laser scanning reference data and merged with UAV-based bathymetry to create a two-year series of seamless digital terrain models. These allow the evaluation of the methodology for conducting high-resolution change analysis of the entire channel. The remote sensing based model of hydromorphology is completed by a new methodology for mapping the flow field in 3D. An acoustic Doppler current profiler (ADCP) is deployed on a remote-controlled boat with a survey-grade global navigation satellite system (GNSS) receiver, allowing the positioning of the areally sampled 3D flow vectors in 3D space as a point cloud and its interpolation into a 3D matrix allows a quantitative volumetric flow analysis. Multitemporal areal 3D flow field data show the evolution of the flow field during a snow-melt flood event. The combination of the underwater and dry topography with the flow field yields a compete model of river hydromorphology at the reach scale.

Initialization of Continuous Nonlinear Models Using Extended Kalman Filter

The two main objectives of Bayesian inference are to estimate parameters and states. In this thesis, we are interested in how this can be done in the framework of state-space models when there is a complete or partial lack of knowledge of the initial state of a continuous nonlinear dynamical system. In literature, similar problems have been referred to as diffuse initialization problems. This is achieved first by extending the previously developed diffuse initialization Kalman filtering techniques for discrete systems to continuous systems. The second objective is to estimate parameters using MCMC methods with a likelihood function obtained from the diffuse filtering. These methods are tried on the data collected from the 1995 Ebola outbreak in Kikwit, DRC in order to estimate the parameters of the system.

Guidelines for small embedded system companies aiming to enter the space industry

This guide summarizes useful information about the European Space Agency (ESA), the European space industry, the ECSS standards and product assurance for small and medium enterprises that are aiming to enter the industry. Additionally, the applicability of agile development in space projects is discussed.

Product Assurance in Agile Space Systems Development

Product assurance is an essential part of product development process if developers want to ensure that final product is safe and reliable. Product assurance can be supported withrisk management and with different failure analysis methods. Product assurance is emphasized in system development process of mission critical systems. The product assurance process in systems of this kind requires extra attention. Inthis thesis, mission critical systems are space systems and the product assurance processof these systems is presented with help of space standards. The product assurance process can be supported with agile development because agile emphasizes transparency of the process and fast response to changes. Even if the development process of space systems is highly standardized and reminds waterfall model, it is still possible to adapt agile development in space systems development. This thesisaims to support the product assurance process of space systems with agile developmentso that the final product would be as safe and reliable as possible. The main purpose of this thesis is to examine how well product assurance is performed in Finnish space organizations and how product assurance tasks and activities can besupported with agile development. The research part of this thesis is performed in survey form.

Product assurance in agile space systems development

Product assurance is an essential part of product development process if developers want to ensure that final product is safe and reliable. Product assurance can be supported with risk management and with different failure analysis methods. Product assurance is emphasized in system development process of mission critical systems. The product assurance process in systems of this kind requires extra attention. In this thesis, mission critical systems are space systems and the product assurance process of these systems is presented with help of space standards. The product assurance process can be supported with agile development because agile emphasizes transparency of the process and fast response to changes. Even if the development process of space systems is highly standardized and reminds waterfall model, it is still possible to adapt agile development in space systems development. This thesis aims to support the product assurance process of space systems with agile development so that the final product would be as safe and reliable as possible. The main purpose of this thesis is to examine how well product assurance is performed in Finnish space organizations and how product assurance tasks and activities can be supported with agile development. The research part of this thesis is performed in survey form.

Grassroots Charity in China: Case Analysis of a Charity Project Organised by Jane Zhang Fan Club

As unregistered grassroots charities do not appear in official statistics in China, they tend to remain unnoticed by scholars. Also as they operate unofficially and avoid publicity, their work is usually not reported by the media. In this research I explore the grassroots charity activity of one pop music fan club from the viewpoint of trust as a sociological concept. I will also establish the general situation on charity in China. By using textual analysis on internet blogs and discussion forums I map the charity project from the discussion of the original idea to the execution and follow up phase. I study the roles the fan club members assume during the project as anonymous participants of internet conversations, as well as concrete active charity volunteers outside of the virtual world. I establish parties, other than the fan club, which are involved in the charity project. Interviews with one of the participant of the project in 2010, 2014 and 2015 bring valuable additional information and help in distributing the questionnaire survey. A quantitative questionnaire survey was distributed among the fan club members to get more detailed information on the motives and attitudes towards official and unofficial charity in China. Because of the inequality in China, the rural minority areas do not have similar educational opportunities as the mostly majority inhabited urban areas, even though the country officially has a nine year compulsory education. Grassroots charities can operate in relative freedom taking some of the government’s burden of social responsibilities if they are not criticizing the authorities. The problem with grassroots charity seems to be lack of sustainability. The lack of trust for authorities and official charities was the reason why the Jane Zhang fan club decided to conduct a charity case unofficially. As a group of people previously unknown to each other, they managed to build mutual trust to carry out the project transparently and successfully, though not sustainably. The internet has provided a new and effective platform for unofficial grassroots charities, who choose not to co-operate with official organisations. On grassroots level charities can have the transparency and trust that lack from official charities. I suggest, that interviewing the real persons behind the internet aliases and finding out what happened outside the discussion forums, would bring a more detailed and outspoken description of the project concerning of the contacts with the local authorities. Also travelling to the site and communicating with the local people in the village would establish how they have experienced the project.

Static waves in corporate space : characterizing oscillating trading patterns in New York stock exchange

Various researches in the field of econophysics has shown that fluid flow have analogous phenomena in financial market behavior, the typical parallelism being delivered between energy in fluids and information on markets. However, the geometry of the manifold on which market dynamics act out their dynamics (corporate space) is not yet known. In this thesis, utilizing a Seven year time series of prices of stocks used to compute S&P500 index on the New York Stock Exchange, we have created local chart to the corporate space with the goal of finding standing waves and other soliton like patterns in the behavior of stock price deviations from the S&P500 index. By first calculating the correlation matrix of normalized stock price deviations from the S&P500 index, we have performed a local singular value decomposition over a set of four different time windows as guides to the nature of patterns that may emerge. I turns out that in almost all cases, each singular vector is essentially determined by relatively small set of companies with big positive or negative weights on that singular vector. Over particular time windows, sometimes these weights are strongly correlated with at least one industrial sector and certain sectors are more prone to fast dynamics whereas others have longer standing waves.

A Business Incubator, Accelerator, or Coworking Space? Case Health Innovation Village at GE

Health Innovation Village at GE is one of the new communities targeted for startup and growth-oriented companies. It has been established at the premises of a multinational conglomerate that will promote networking and growth of startup companies. The concept combines features from traditional business incubators, accelerators, and coworking spaces. This research compares Health Innovation Village to these concepts regarding its goals, target clients, source of income, organization, facilities, management, and success factors. In addition, a new incubator classification model is introduced. On the other hand, Health Innovation Village is examined from its tenants’ perspective and improvements are suggested. The work was implemented as a qualitative case study by interviewing GE staff with connections to Health Innovation Village as well as startup entrepreneurs and employees’ working there. The most evident features of Health Innovation Village correspond to those of business incubators although it is atypical as a non-profit corporate business incubator. Strong network orientation and connections to venture capitalists are common characteristics of these new types of accelerators. The design of the premises conforms to the principles of coworking spaces, but the services provided to the startup companies are considerably more versatile than the services offered by coworking spaces. The advantages of Health Innovation Village are that there are first-class premises and exceptionally good networking possibilities that other types of incubators or accelerators are not able to offer. A conglomerate can also provide multifaceted special knowledge for young firms. In addition, both GE and the startups gained considerable publicity through their cooperation, indeed a characteristic that benefits both parties. Most of the expectations of the entrepreneurs were exceeded. However, communication and the scope of cooperation remain challenges. Micro companies spend their time developing and marketing their products and acquiring financing. Therefore, communication should be as clear as possible and accessible everywhere. The startups would prefer to cooperate significantly more, but few have the time available to assume the responsibility of leadership. The entrepreneurs also expected to have more possibilities for cooperation with GE. Wider collaboration might be accomplished by curation in the same way as it is used in the well-functioning coworking spaces where curators take care of practicalities and promote cooperation. Communication issues could be alleviated if the community had its own Intranet pages where all information could be concentrated. In particular, a common calendar and a room reservation system could be useful. In addition, it could be beneficial to have a section of the Intranet open for both the GE staff and the startups so that those willing to share their knowledge and those having project offers could use it for advertising.