Stress testing and risk evaluation of new capacity payment algorithm proposed by Market Council

In the Russian Wholesale Market, electricity and capacity are traded separately. Capacity is a special good, the sale of which obliges suppliers to keep their generating equipment ready to produce the quantity of electricity indicated by the System Operator. The purpose of the formation of capacity trading was the maintenance of reliable and uninterrupted delivery of electricity in the wholesale market. The price of capacity reflects constant investments in construction, modernization and maintenance of power plants. So, the capacity sale creates favorable conditions to attract investments in the energy sector because it guarantees the investor that his investments will be returned.

Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Travelling in a Palimpsest : Finnish nineteenth-century painters' encounters with Spanish art and culture

Utgångspunkten för avhandlingen är finländska konstnärsresor till Spanien under 1800-talet, och kontakterna med spansk konst och kultur. Endast ett fåtal finländare reste till Spanien, och inledningsvis utrycktes intresset för spansk konst i form av kopior efter gamla mästare, utförda både efter original utanför Spanien, och reproduktioner. Denna föga imponerande start efterföljdes av ett litet antal målare som verkligen reste till Spanien under 1800-talets senare hälft: Adolf von Becker (1831–1909), Albert Edelfelt (1854–1905) och Venny Soldan (1863–1945). Jag undersöker hur deras syn på landet manifesterades i deras resebilder i förhållande till den växande turistindustrin. Syftet med avhandlingen är att visa hur den resande målaren, likt en turist, föreställde sig, upplevde och tolkade den främmande kulturen, och hur detta avbildades och uttrycktes i deras resebilder. Vid sidan av ikonografisk analys och stilkritik utnyttjas forskningsmetoder från turismteorin. Resultatet av undersökningen visar att de flesta konstnärerna dyrkade konsten på Prado-museet, beundrade flamenco, Andalusiens vackra kvinnor, tjurfäktningar och zigenarna. De längtade efter en förgången och exotisk tid, samtidigt som de följde de vältrampade turiststigarna och hänfördes av de sedvanliga sevärdheterna; de reste i ett delvis mytiskt och delvis verkligt land. Likt turister (i allmänhet), såg de det de ville se, och sökte sig till på förhand inpräntade mentala (före)bilder. Resebilderna kan med fog tolkas som medvetet konstruerade minnen från resan, souvenirs d’Espagne. Samtidigt förstärkte och upprätthöll valen av motiv uppfattningen att Spaniens äldre konst och samtida kultur var mer ”äkta” (autentiska) än den kultur man själv tillhörde. Spanien uppfattades som en kvarleva från en förgången tid som hölls levande i nuet

Den etiske akten : den caritative etikken når pasientens fordringer er av eksistensiell art

The purpose of this thesis is to develop a theory model about some core concepts and phenomena within caritative ethics when patients' demands are existential. There are two research questions, (A) Which realities represent concepts such courage, responsibility, and sacrifice within the caritative ethics. (B) Which phenomena of ethical significance are made current and applicable when patients¿ demands are existential. This study takes as its point of departurecertain chosen theoretical perspectives that discuss some perspectives of the concepts of courage, responsibility, and sacrifice in terms of their significanceto the research questions A. This represents the study¿s theoretical data. The empirical data provide answers to the research question B. In the end, the thesis discusses synthesis of these two accesses of knowledge in order to formulate theses and create a theory model. Løgstrup's contribution and description of the ethical claim helps in understanding and interpreting the links between the substance of the caritative ethic and the concrete reality in the encounter with existential issues. This thesis is a study within the field of Caring Science. The nursing profession provides empirical data and reflects the study topic, by addressing issues of relevance to the application of the knowledge of Caring Sciencein light of the nursing profession's various daily challenges. This study proceeds from the basic assumption: "Caring relationships form the meaningful contextfor caring and derive from the ethos of love, responsibility, and sacrifice, i.e. a caritative ethics" (Eriksson 2001). This study attempts to explore and prove this statement in the light of theoretical and empirical data, in the light ofthe caring scientific perspective which is here linked particularly to the viewof man as a unity of body, mind, and soul, and to the ontological health model. Hermeneutics is the overall perspective for the interpretations proposed in this thesis. Through conversation and hermeneutic observations, I try to understandthe challenges of nursing performance in the encounter with existential issues. This constitutes the empirical data that was gathered on a ward treating cancerpatients. The discussion proceeds sequence by sequence, first by discussing theconditions of the caritative ethics when meeting the existential claims in the light of the concepts of courage, sacrifice, and responsibility. Then a thesis is formulated concerning the caritative ethics in the light of Caring Science. This is the foundation of the creation of the theory model. The resulting theses concern the chosen concepts and phenomena which promote caritative ethics when patients' claims are existential: Freedom is the hallmark of caritative ethics. Freedom is the basic category of caring. When attending to the patient's existential claims, it is of vital importance to secure human relationships as caring interpersonal communions, created by responsible persons who have shown courage and sacrifice. Courage and sacrifice constitute the ethos of caring communities (communions). Courage and sacrifice are then a part of the collective ethos of caring communities, because the patient is confirmed as the unity of body, mind, and soul.

Reise-Beschreibung von Lappland und Bothnien : worinnen nicht nur von der Landes-Art, Winter und Sommer, Nord-Licht oder Nord-Schein, Mineralien, Gewächsen, Thieren, wie auch der Einwohner Beschaffenheit, Religion, Gouvernement, Kauffmannschafft, Wohnungen, Jagden, und andern denckwürdigen Dingen, aus selbsteigenen Augenschein und Erfahrung durch einige Figuren gezeiget; sondern auch die dahin und wieder von dar zurück genommene Reise ordentlich dargeleget wird : von Johann Gerhard Schellern, h.t. Pastore zu Hermstedt und Stober.

Digital reproduction, The National Library of Finland, Centre for Preservation and Digitisation, Mikkeli

Herrn Johann Gerhard Schellers, ehemaligen Pastoris zu Hermstedt und Stobra Reise-Beschreibung nach Lappland und Bothnien : worinnen sowohl die dasige Landes-Art in deutlichen Abtheilungen und nöthigen Figuren aus eigenem Augenschein, gezeiget, als auch die Gelegenheit zur Reise und Rückreise kürtzlich angeführet wird : abermahls dem Druck übergeben von Gottlieb David Friedrich Scheller Rev. Min. Candid.

Digital reproduction, The National Library of Finland, Centre for Preservation and Digitisation, Mikkeli

Solving Leontief Input-Output Model with Trapezoidal Fuzzy Numbers and Gauss-Seidel Algorithm

In this work a fuzzy linear system is used to solve Leontief input-output model with fuzzy entries. For solving this model, we assume that the consumption matrix from di erent sectors of the economy and demand are known. These assumptions heavily depend on the information obtained from the industries. Hence uncertainties are involved in this information. The aim of this work is to model these uncertainties and to address them by fuzzy entries such as fuzzy numbers and LR-type fuzzy numbers (triangular and trapezoidal). Fuzzy linear system has been developed using fuzzy data and it is solved using Gauss-Seidel algorithm. Numerical examples show the e ciency of this algorithm. The famous example from Prof. Leontief, where he solved the production levels for U.S. economy in 1958, is also further analyzed.

Contemporary art galleries innovation management

This paper focuses on capabilities implemented by micro firms in actual art sector. After last two decades, since establishment of new art selling ventures has started, current art market of Russia is still in its emerging phase. Art galleries, who preserve to be the main place where the art is purchased, today have to survive in the hostile business environment. Whereas the rivalry does not affect gallery performance significantly, the major challenges for these micro firms are customer unawareness and shortages of financing. The business environment requires capabilities inherited by galleries to sustain the performance. Such capabilities may lead to innovation adoption. This paper represents the first explorative study on contemporary art market of Saint-Petersburg. In order to gain an understanding of the topic, qualitative method was chosen and in-depth interviews were done with 7 different micro firms using key informant method.

GAMS MINLP Solver comparisons and some improvements to the AlphaECP algorithm

I doktorsavhandlingen undersöks förmågan att lösa hos ett antal lösare för optimeringsproblem och ett antal svårigheter med att göra en rättvis lösarjämförelse avslöjas. Dessutom framläggs några förbättringar som utförts på en av lösarna som heter GAMS/AlphaECP. Optimering innebär, i det här sammanhanget, att finna den bästa möjliga lösningen på ett problem. Den undersökta klassen av problem kan karaktäriseras som svårlöst och förekommer inom ett flertal industriområden. Målet har varit att undersöka om det finns en lösare som är universellt snabbare och hittar lösningar med högre kvalitet än någon av de andra lösarna. Det kommersiella optimeringssystemet GAMS (General Algebraic Modeling System) och omfattande problembibliotek har använts för att jämföra lösare. Förbättringarna som presenterats har utförts på GAMS/AlphaECP lösaren som baserar sig på skärplansmetoden Extended Cutting Plane (ECP). ECP-metoden har utvecklats främst av professor Tapio Westerlund på Anläggnings- och systemteknik vid Åbo Akademi.

Exploration and Design of Power-Efficient Networked Many-Core Systems

Multiprocessing is a promising solution to meet the requirements of near future applications. To get full benefit from parallel processing, a manycore system needs efficient, on-chip communication architecture. Networkon- Chip (NoC) is a general purpose communication concept that offers highthroughput, reduced power consumption, and keeps complexity in check by a regular composition of basic building blocks. This thesis presents power efficient communication approaches for networked many-core systems. We address a range of issues being important for designing power-efficient manycore systems at two different levels: the network-level and the router-level. From the network-level point of view, exploiting state-of-the-art concepts such as Globally Asynchronous Locally Synchronous (GALS), Voltage/ Frequency Island (VFI), and 3D Networks-on-Chip approaches may be a solution to the excessive power consumption demanded by today’s and future many-core systems. To this end, a low-cost 3D NoC architecture, based on high-speed GALS-based vertical channels, is proposed to mitigate high peak temperatures, power densities, and area footprints of vertical interconnects in 3D ICs. To further exploit the beneficial feature of a negligible inter-layer distance of 3D ICs, we propose a novel hybridization scheme for inter-layer communication. In addition, an efficient adaptive routing algorithm is presented which enables congestion-aware and reliable communication for the hybridized NoC architecture. An integrated monitoring and management platform on top of this architecture is also developed in order to implement more scalable power optimization techniques. From the router-level perspective, four design styles for implementing power-efficient reconfigurable interfaces in VFI-based NoC systems are proposed. To enhance the utilization of virtual channel buffers and to manage their power consumption, a partial virtual channel sharing method for NoC routers is devised and implemented. Extensive experiments with synthetic and real benchmarks show significant power savings and mitigated hotspots with similar performance compared to latest NoC architectures. The thesis concludes that careful codesigned elements from different network levels enable considerable power savings for many-core systems.

On state and parameter estimation in chaotic systems

State-of-the-art predictions of atmospheric states rely on large-scale numerical models of chaotic systems. This dissertation studies numerical methods for state and parameter estimation in such systems. The motivation comes from weather and climate models and a methodological perspective is adopted. The dissertation comprises three sections: state estimation, parameter estimation and chemical data assimilation with real atmospheric satellite data. In the state estimation part of this dissertation, a new filtering technique based on a combination of ensemble and variational Kalman filtering approaches, is presented, experimented and discussed. This new filter is developed for large-scale Kalman filtering applications. In the parameter estimation part, three different techniques for parameter estimation in chaotic systems are considered. The methods are studied using the parameterized Lorenz 95 system, which is a benchmark model for data assimilation. In addition, a dilemma related to the uniqueness of weather and climate model closure parameters is discussed. In the data-oriented part of this dissertation, data from the Global Ozone Monitoring by Occultation of Stars (GOMOS) satellite instrument are considered and an alternative algorithm to retrieve atmospheric parameters from the measurements is presented. The validation study presents first global comparisons between two unique satellite-borne datasets of vertical profiles of nitrogen trioxide (NO3), retrieved using GOMOS and Stratospheric Aerosol and Gas Experiment III (SAGE III) satellite instruments. The GOMOS NO3 observations are also considered in a chemical state estimation study in order to retrieve stratospheric temperature profiles. The main result of this dissertation is the consideration of likelihood calculations via Kalman filtering outputs. The concept has previously been used together with stochastic differential equations and in time series analysis. In this work, the concept is applied to chaotic dynamical systems and used together with Markov chain Monte Carlo (MCMC) methods for statistical analysis. In particular, this methodology is advocated for use in numerical weather prediction (NWP) and climate model applications. In addition, the concept is shown to be useful in estimating the filter-specific parameters related, e.g., to model error covariance matrix parameters.

Defining the art of grammar: Ancient perceptions of γραμματική and grammatical

The subject of this dissertation, which belongs to the field of Classical Philology, are the definitions of the art of grammar found in Greek and Latin sources from the Classical era to the second century CE. Definitions survive from grammarians, philosophers, and general scholars. I have examined these definitions from two main points of view: how they are formed, and how they reflect the development of the art itself. Defining formed part of dialectic, in practice also of rhetoric, and was perceived as important from the Classical era onwards. Definitions of grammar seem to have become established as part of preliminary discussions, located at the beginning of grammatical manuals (tékhnai, artes). These discussions included certain principal notions of the art; in addition to the definition, a list of the parts of the art was also typically included. These lists were formed by two different methods: division (diaíresis, divisio) and partition (merismós, partitio). Many of the grammarians may actually have been unfamiliar with these methods, unlike the two most important scholars of the Late Republic, Varro and Cicero. Significant attention was devoted to the question whether the art of grammar is based on lógos or empeiría. This epistemological question had its roots in medical theories, which were prominent in Alexandria. In the history of the concept of grammatiké or grammatica, three stages become evident. In the Classical era, the Greek term is used to refer to a very concrete art of letters (grámmata); from the Hellenistic era onwards it refers to the art developed by the Alexandrian scholars, a matter of textual and literary criticism. Towards the end of the Hellenistic era, the grammarian also becomes involved with the question of correct language, which gradually begins to appear in the definitions as well.

Thermal-Aware Networked Many-Core Systems

Advancements in IC processing technology has led to the innovation and growth happening in the consumer electronics sector and the evolution of the IT infrastructure supporting this exponential growth. One of the most difficult obstacles to this growth is the removal of large amount of heatgenerated by the processing and communicating nodes on the system. The scaling down of technology and the increase in power density is posing a direct and consequential effect on the rise in temperature. This has resulted in the increase in cooling budgets, and affects both the life-time reliability and performance of the system. Hence, reducing on-chip temperatures has become a major design concern for modern microprocessors. This dissertation addresses the thermal challenges at different levels for both 2D planer and 3D stacked systems. It proposes a self-timed thermal monitoring strategy based on the liberal use of on-chip thermal sensors. This makes use of noise variation tolerant and leakage current based thermal sensing for monitoring purposes. In order to study thermal management issues from early design stages, accurate thermal modeling and analysis at design time is essential. In this regard, spatial temperature profile of the global Cu nanowire for on-chip interconnects has been analyzed. It presents a 3D thermal model of a multicore system in order to investigate the effects of hotspots and the placement of silicon die layers, on the thermal performance of a modern ip-chip package. For a 3D stacked system, the primary design goal is to maximise the performance within the given power and thermal envelopes. Hence, a thermally efficient routing strategy for 3D NoC-Bus hybrid architectures has been proposed to mitigate on-chip temperatures by herding most of the switching activity to the die which is closer to heat sink. Finally, an exploration of various thermal-aware placement approaches for both the 2D and 3D stacked systems has been presented. Various thermal models have been developed and thermal control metrics have been extracted. An efficient thermal-aware application mapping algorithm for a 2D NoC has been presented. It has been shown that the proposed mapping algorithm reduces the effective area reeling under high temperatures when compared to the state of the art.