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.

Causation and dominance : a study of Finnish causative verbs expressing social dominance

En väsentlig fråga inom såväl lingvistiska som kognitiva teorier är, hur språket beskriver kausala relationer. I finskan finns det en speciell typ av kausativa verb avledda med suffixet (U)ttA som används för att uttrycka att handlingen i fråga utförs av någon annan än subjektreferenten, t.ex. Maija haetuttaa Matilla kirjastosta kirjan ’Maija låter Matti hämta boken från biblioteket’ och Matti juoksuttaa Maijan kaupunkiin ’Matti låter Maija springa till staden’. Syftet med denna avhandling var att med exempel av sociala dominansens kausativer undersöka ordbildningens natur samt begreppet ’socialt förorsakande’. För att beskriva avledningars regelbundna argumentstruktur i form av kopplingen mellan syntaxen och semantiken upprättades deras prototypiska strukturer. Dessa verb har emellertid också specifika användningsområden som framhäver variationer i sociala relationer. Säregna egenskaper hos den sociala dominansens kausativer inkluderades i undersökningen och definierades som konstruktioner. Konstruktionerna omfattar speciella syntaktiska och/eller semantiska element och utöver det också pragmatiska värderande implikationer. Uppbyggnaden av den sociala dimensionen hos de undersökta verben består av egenskaper förbundna med typen av förorsakande, argumentens agentiva egenskaper (aktivitet eller passivitet, dominans, kontroll, viljestyrdhet och ansvarighet) samt konventionaliserade attityder och tolkningar. Ett exempel på en s.k. 'tolkningskonstruktion’ är den negativa dominansens uttryck som i avhandlingen kallas Maktmissbrukskonstruktionen. Denna konstruktion inkluderar talarens starkt kritiska hållning till den uttryckta situationen, t.ex. Asiakas juoksuttaa lentoemäntää ’Kunden låter flygvärdinnan springa’. Dessa konstruktioner fyller en viktig funktion i språklig kommunikation: att beskriva avvikande av sociala normer och att foga expressivitet till budskapet. Metodologiskt kombinerar denna avhandling teorier som baseras på det aktuella språkbruket och teoretisk lingvistisk analys. Verbens samt konstruktionernas konceptuella lexikala struktur och prototypstrukturerna analyserades med hjälp av den konceptuella semantikens verktyg, som har utvecklats av Jackendoff, Nikanne och Pörn.

The Structural Basis for inorganic Pyrophosphatase Catalysis and Regulation

Inorganic pyrophosphatases (PPases) are essential enzymes for every living cell. PPases provide the necessary thermodynamic pull for many biosynthetic reactions by hydrolyzing pyrophosphate. There are two types of PPases: integral membrane-bound and soluble enzymes. The latter type is divided into two non-homologous protein families, I and II. Family I PPases are present in all kingdoms of life, whereas family II PPases are only found in prokaryotes, including archae. Family I PPases, particularly that from Saccharomyces cerevisiae, are among the most extensively characterized phosphoryl transfer enzymes. In the present study, we have solved the structures of wild-type and seven active site variants of S. cerevisiae PPase bound to its natural metal cofactor, magnesium ion. These structures have facilitated derivation of the complete enzyme reaction scheme for PPase, fulfilling structures of all the reaction intermediates. The main focus in this study was on a novel subfamily of family II PPases (CBSPPase) containing a large insert formed by two CBS domains and a DRTGG domain within the catalytic domain. The CBS domain (named after cystathionine beta-synthase in which it was initially identified) usually occurs as tandem pairs with two or four copies in many proteins in all kingdoms of life. The structure formed by a pair of CBS domains is also known as a Bateman domain. CBS domains function as regulatory units, with adenylate ligands as the main effectors. The DRTGG domain (designated based on its most conserved residues) occurs less frequently and only in prokaryotes. Often, the domain co-exists with CBS domains, but its function remains unknown. The key objective of the current study was to explore the structural rearrangements in the CBS domains induced by regulatory adenylate ligands and their functional consequences. Two CBS-PPases were investigated, one from Clostridium perfringens (cpCBS-PPase) containing both CBS and DRTGG domains in its regulatory region and the other from Moorella thermoacetica (mt CBS-PPase) lacking the DRTGG domain. We additionally constructed a separate regulatory region of cpCBS-PPase (cpCBS). Both full-length enzymes and cpCBS formed homodimers. Two structures of the regulatory region of cpCBS-PPase complexed with the inhibitor, AMP, and activator, diadenosine tetraphosphate, were solved. The structures were significantly different, providing information on the structural pathway from bound adenylates to the interface between the regulatory and catalytic parts. To our knowledge, these are the first reported structures of a regulated CBS enzyme, which reveal large conformational changes upon regulator binding. The activator-bound structure was more open, consistent with the different thermostabilities of the activator- and inhibitor-bound forms of cpCBS-PPase. The results of the functional studies on wild-type and variant CBS-PPases provide support for inferences made on the basis of structural analyses. Moreover, these findings indicate that CBS-PPase activity is highly sensitive to adenine nucleotide distribution between AMP, ADP and ATP, and hence to the energy level of the cell. CBS-PPase activity is markedly inhibited at low energy levels, allowing PPi energy to be used for cell survival instead of being converted into heat.

Esiopetuskirjojen harjoitukset kielellisen tietoisuuden kehittäjinä

Tutkimus oli kasvatustieteellinen varhaiskasvatuksen alan tutkimus, jossa hyödynnettiin kielitieteellistä käsitteistöä. Tutkimuksen kohteena olivat esiopetuskirjojen kielellisen tietoisuuden harjoitukset. Aineistona oli 12 esiopetuksen harjoituskirjaa ja opettajan opasta. Kirjoissa oli yhteensä yli 2000 sivua ja yli 1300 harjoitusta. Tarkemmassa analyysissä olleiden harjoitusten määrä oli noin 460. Analyysimenetelmänä käytettiin sisällönanalyysiä, jonka avulla tutkittiin, millaisia kielellisen tietoisuuden harjoituksia esiopetuskirjoissa oli ja miten harjoitukset etenivät. Kielellisen tietoisuuden harjoitukset luokiteltiin fonologisen, morfologisen ja syntaktisen tietoisuuden harjoituksiin. Fonologinen tietoisuus käsitettiin lapsen kyvyksi havaita ja käsitellä kielen äännerakennetta. Morfologisella tietoisuudella tarkoitettiin kykyä havaita ja käsitellä kielen morfeemeja eli pienimpiä merkityksellisiä osia. Syntaktisella tietoisuudella tarkoitettiin lapsen tietoisuutta siitä, miten lauseet rakentuvat. Olennaisiksi piirteiksi fonologisen tietoisuuden harjoituksissa identifioituivat harjoitusten edellyttämä tai harjoittama tietoisuuden taso, harjoitusten kohteena olevien lingvististen yksiköiden taso ja harjoitustyyppi sekä morfologisen ja syntaktisen tietoisuuden harjoituksissa tietoisuuden taso ja harjoitustyyppi. Tutkimuksessa luotiin aikaisempien tutkimusten pohjalta mallit siitä, miten eri harjoitukset etenisivät optimaalisesti lapsen kielellisen tietoisuuden kehittymisen kannalta. Eri harjoituskirjojen harjoitusten etenemistä verrattiin näihin malleihin. Fonologisen tietoisuuden harjoituksista voitiin tunnistaa viisi päätyyppiä, joista useat jakautuivat vielä alatyypeiksi. Harjoitusten alatyypit ilmaisivat yleensä harjoituksissa käytettävän kognitiivisen operaation – käytettiinkö harjoituksessa tunnistamista, yhdistämistä vai osiin jakamista. Tämä samoin kuin harjoituksessa käytetty lingvistinen yksikkö (sana, loppusointu, tavu tai äänne) ja tietoisuuden taso olivat yhteydessä harjoituksen vaikeuteen. Tutkimuksissa ja interventioissa esiopetusikäisilläkin käytettyjä muunteluharjoituksia, joissa sanasta tai tavusta poistetaan osa, siihen lisätään osa tai osaa siirretään, harjoituskirjoissa ei ollut. Morfologisen tietoisuuden harjoitukset kohdistuivat yhdyssanoihin, taivutuspäätteisiin tai johdoksiin. Syntaktisen tietoisuuden harjoituksista identifioitui yhdentoista harjoituslajin alatyypin kautta kuusi päätyyppiä. Tutkimusta voidaan hyödyntää esiopetuskirjojen arvioinnissa ja laatimisessa sekä varhaiskasvatus- ja esiopetuspedagogiikassa.

Tekijännimet Mikael Agricolan teosten kielessä. Henkilötarkoitteisten johdosten merkitykset, funktiot ja rakenteet

My research deals with agent nouns in the language of the works of Mikael Agricola (ca. 1510–1557). The main tasks addressed in my thesis have been to describe individual agent noun types, to provide a comprehensive picture of the category of agent nouns and to clarify the relations between different types of agent nouns. My research material consists of all the agent nouns referring to persons in the language of Agricola’s works, together with their context. The language studied is for the most part translated language. Agent nouns play an important role both in the vocabulary of natural language and in broader sentence structures, since in a text it is constantly necessary to refer to actors re-ferring to persons in the text. As a concept and a phenomenon, the agent noun is widely known in languages. It is a word formed with a certain derivational affixes, which typical-ly refers to a person. In my research the agent noun category includes both deverbal and denominal derivatives referring to persons, e.g. kirjoittaa > kirjoittaja (to write > writer), asua > asuva (to inhabit > inhabitant), imeä > imeväinen (to suck > suckling), juopua > juopunut (to drink > drunkard), pelätä > pelkuri (to fear > one who fears ‘a coward’), apu > apulainen (help/to help > helper); lammas > lampuri (sheep > shepherd). Besides original Finnish expressions, agent noun derivatives taken as such from foreign languages form a word group of central importance for the research (e.g. nikkari, porvari, ryöväri, based on the German/Swedish for carpenter, burgher, robber). Especially important for the formation of agent nouns in Finnish are the models offered by foreign languages. The starting point for my work is predominantly semantic, as both the criteria for collecting the material and the categorisation underlying the analysis of the material are based on semantic criteria. When examining derivatives, aspects relating to structure are also inevitably of central importance, as form and meaning are closely associated with each other in this type of vocabulary. The alliance of structure and meaning can be described in an illustrative manner with the help of structural schemata. The examination of agent nouns comprises on the one hand analysis of syntactic elements and on the other, study of cultural words in their most typical form. The latter aspect offers a research object in which language and the extralinguistic world, referents, their designations and cultural-historical reality are in concrete terms one and the same. Thus both the agent noun types that follow the word formation principles of the Finn-ish language and those of foreign origin borrowed as a whole into Finnish illustrate very well how an expression of a certain origin and formed according to a certain structural model is inseparably bound up with the background of its referent and in general with semantic factors. This becomes evident both on the level of the connection between cer-tain linguistic features and text genre and in relation to cultural words referring to per-sons. For example, the model for the designations of God based on agent nouns goes back thousands of years and is still closely linked in 16th century literature with certain text genres. This brings out the link between the linguistic feature and the genre in a very con-crete manner. A good example of the connection between language and the extralinguistic world is provided by the cultural vocabulary referring to persons. Originally Finnish agent noun derivatives are associated with an agrarian society, while the vocabulary relat-ing to mediaeval urbanisation, the Hansa trade and specialisation by trade or profession is borrowed and originates in its entirety from vocabulary that was originally German.

Trustworthy context dependency in ubiquitous systems

The modern society is getting increasingly dependent on software applications. These run on processors, use memory and account for controlling functionalities that are often taken for granted. Typically, applications adjust the functionality in response to a certain context that is provided or derived from the informal environment with various qualities. To rigorously model the dependence of an application on a context, the details of the context are abstracted and the environment is assumed stable and fixed. However, in a context-aware ubiquitous computing environment populated by autonomous agents, a context and its quality parameters may change at any time. This raises the need to derive the current context and its qualities at runtime. It also implies that a context is never certain and may be subjective, issues captured by the context’s quality parameter of experience-based trustworthiness. Given this, the research question of this thesis is: In what logical topology and by what means may context provided by autonomous agents be derived and formally modelled to serve the context-awareness requirements of an application? This research question also stipulates that the context derivation needs to incorporate the quality of the context. In this thesis, we focus on the quality of context parameter of trustworthiness based on experiences having a level of certainty and referral experiences, thus making trustworthiness reputation based. Hence, in this thesis we seek a basis on which to reason and analyse the inherently inaccurate context derived by autonomous agents populating a ubiquitous computing environment in order to formally model context-awareness. More specifically, the contribution of this thesis is threefold: (i) we propose a logical topology of context derivation and a method of calculating its trustworthiness, (ii) we provide a general model for storing experiences and (iii) we formalise the dependence between the logical topology of context derivation and its experience-based trustworthiness. These contributions enable abstraction of a context and its quality parameters to a Boolean decision at runtime that may be formally reasoned with. We employ the Action Systems framework for modelling this. The thesis is a compendium of the author’s scientific papers, which are republished in Part II. Part I introduces the field of research by providing the mending elements for the thesis to be a coherent introduction for addressing the research question. In Part I we also review a significant body of related literature in order to better illustrate our contributions to the research field.

Adaptive control of Hydraulic Drive

Adaptive control systems are one of the most significant research directions of modern control theory. It is well known that every mechanical appliance’s behavior noticeably depends on environmental changes, functioning-mode parameter changes and changes in technical characteristics of internal functional devices. An adaptive controller involved in control process allows reducing an influence of such changes. In spite of this such type of control methods is applied seldom due to specifics of a controller designing. The work presented in this paper shows the design process of the adaptive controller built by Lyapunov’s function method for the Hydraulic Drive. The calculation needed and the modeling were conducting with MATLAB® software including Simulink® and Symbolic Math Toolbox™ etc. In the work there was applied the Jacobi matrix linearization of the object’s mathematical model and derivation of the suitable reference models based on Newton’s characteristic polynomial. The intelligent adaptive to nonlinearities algorithm for solving Lyapunov’s equation was developed. Developed algorithm works properly but considered plant is not met requirement of functioning with. The results showed confirmation that adaptive systems application significantly increases possibilities in use devices and might be used for correction a system’s behavior dynamics.

A systematic mapping study of web services discovery mechanisms

Context: Web services have been gaining popularity due to the success of service oriented architecture and cloud computing. Web services offer tremendous opportunity for service developers to publish their services and applications over the boundaries of the organization or company. However, to fully exploit these opportunities it is necessary to find efficient discovery mechanism thus, Web services discovering mechanism has attracted a considerable attention in Semantic Web research, however, there have been no literature surveys that systematically map the present research result thus overall impact of these research efforts and level of maturity of their results are still unclear. This thesis aims at providing an overview of the current state of research into Web services discovering mechanism using systematic mapping. The work is based on the papers published 2004 to 2013, and attempts to elaborate various aspects of the analyzed literature including classifying them in terms of the architecture, frameworks and methods used for web services discovery mechanism. Objective: The objective if this work is to summarize the current knowledge that is available as regards to Web service discovery mechanisms as well as to systematically identify and analyze the current published research works in order to identify different approaches presented. Method: A systematic mapping study has been employed to assess the various Web Services discovery approaches presented in the literature. Systematic mapping studies are useful for categorizing and summarizing the level of maturity research area. Results: The result indicates that there are numerous approaches that are consistently being researched and published in this field. In terms of where these researches are published, conferences are major contributing publishing arena as 48% of the selected papers were conference published papers illustrating the level of maturity of the research topic. Additionally selected 52 papers are categorized into two broad segments namely functional and non-functional based approaches taking into consideration architectural aspects and information retrieval approaches, semantic matching, syntactic matching, behavior based matching as well as QOS and other constraints.

Altaica from Harrassowitz

Kirjallisuusarvostelu

Adaptive Dynamics of Resource Specialization

Ecological specialization in resource utilization has various facades ranging from nutritional resources via host use of parasites or phytophagous insects to local adaptation in different habitats. Therefore, the evolution of specialization affects the evolution of most other traits, which makes it one of the core issues in the theory of evolution. Hence, the evolution of specialization has gained enormous amounts of research interest, starting already from Darwin’s Origin of species in 1859. Vast majority of the theoretical studies has, however, focused on the mathematically most simple case with well-mixed populations and equilibrium dynamics. This thesis explores the possibilities to extend the evolutionary analysis of resource usage to spatially heterogeneous metapopulation models and to models with non-equilibrium dynamics. These extensions are enabled by the recent advances in the field of adaptive dynamics, which allows for a mechanistic derivation of the invasion-fitness function based on the ecological dynamics. In the evolutionary analyses, special focus is set to the case with two substitutable renewable resources. In this case, the most striking questions are, whether a generalist species is able to coexist with the two specialist species, and can such trimorphic coexistence be attained through natural selection starting from a monomorphic population. This is shown possible both due to spatial heterogeneity and due to non-equilibrium dynamics. In addition, it is shown that chaotic dynamics may sometimes inflict evolutionary suicide or cyclic evolutionary dynamics. Moreover, the relations between various ecological parameters and evolutionary dynamics are investigated. Especially, the relation between specialization and dispersal propensity turns out to be counter-intuitively non-monotonous. This observation served as inspiration to the analysis of joint evolution of dispersal and specialization, which may provide the most natural explanation to the observed coexistence of specialist and generalist species.

Capital investments planning and life cycle simulations for the new valves manufacturing facility in Russia

The focus of the research is on the derivation of the valid and reliable performance results regarding establishment and launching of the new full-scale industrial facility, considering the overall current conditions for the project realization in and out of Russia. The study demonstrates the process of the new facility concept development, with following perfor-mance calculation, comparative analyzes conduction, life-cycle simulations, performance indicators derivation and project`s sustainability evaluation. To unite and process the entire input parameters complexity, regards the interlacing between the project`s internal technical and commercial sides on the one hand, and consider all the specifics of the Russian conditions for doing business on the other hand, was developed the unique model for the project`s performance calculation, simulations and results representation. The complete research incorporates all corresponding data to substantiate the assigned facility`s design, sizing and output capacity for high quality and cost efficient ferrous pipe-line accessories manufacturing, as well as, demonstrates that this project could be suc-cessfully realized in current conditions in Russia and highlights the room for significant performance and sustainability improvements based on the indexes of the derived KPIs.