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.

Teaching mathematics and programming : new approaches with empirical evaluation

Programming and mathematics are core areas of computer science (CS) and consequently also important parts of CS education. Introductory instruction in these two topics is, however, not without problems. Studies show that CS students find programming difficult to learn and that teaching mathematical topics to CS novices is challenging. One reason for the latter is the disconnection between mathematics and programming found in many CS curricula, which results in students not seeing the relevance of the subject for their studies. In addition, reports indicate that students' mathematical capability and maturity levels are dropping. The challenges faced when teaching mathematics and programming at CS departments can also be traced back to gaps in students' prior education. In Finland the high school curriculum does not include CS as a subject; instead, focus is on learning to use the computer and its applications as tools. Similarly, many of the mathematics courses emphasize application of formulas, while logic, formalisms and proofs, which are important in CS, are avoided. Consequently, high school graduates are not well prepared for studies in CS. Motivated by these challenges, the goal of the present work is to describe new approaches to teaching mathematics and programming aimed at addressing these issues: Structured derivations is a logic-based approach to teaching mathematics, where formalisms and justifications are made explicit. The aim is to help students become better at communicating their reasoning using mathematical language and logical notation at the same time as they become more confident with formalisms. The Python programming language was originally designed with education in mind, and has a simple syntax compared to many other popular languages. The aim of using it in instruction is to address algorithms and their implementation in a way that allows focus to be put on learning algorithmic thinking and programming instead of on learning a complex syntax. Invariant based programming is a diagrammatic approach to developing programs that are correct by construction. The approach is based on elementary propositional and predicate logic, and makes explicit the underlying mathematical foundations of programming. The aim is also to show how mathematics in general, and logic in particular, can be used to create better programs.

Enabling constructive alignment in programming instruction

In this thesis, simple methods have been sought to lower the teacher’s threshold to start to apply constructive alignment in instruction. From the phases of the instructional process, aspects that can be improved with little effort by the teacher have been identified. Teachers have been interviewed in order to find out what students actually learn in computer science courses. A quantitative analysis of the structured interviews showed that in addition to subject specific skills and knowledge, students learn many other skills that should be mentioned in the learning outcomes of the course. The students’ background, such as their prior knowledge, learning style and culture, affects how they learn in a course. A survey was conducted to map the learning styles of computer science students and to see if their cultural background affected their learning style. A statistical analysis of the data indicated that computer science students are different learners than engineering students in general and that there is a connection between the student’s culture and learning style. In this thesis, a simple self-assessment scale that is based on Bloom’s revised taxonomy has been developed. A statistical analysis of the test results indicates that in general the scale is quite reliable, but single students still slightly overestimate or under-estimate their knowledge levels. For students, being able to follow their own progress is motivating, and for a teacher, self-assessment results give information about how the class is proceeding and what the level of the students’ knowledge is.

Computational modeling for irrigated agriculture planning. Part I: general description and linear programming

Linear programming models are effective tools to support initial or periodic planning of agricultural enterprises, requiring, however, technical coefficients that can be determined using computer simulation models. This paper, presented in two parts, deals with the development, application and tests of a methodology and of a computational modeling tool to support planning of irrigated agriculture activities. Part I aimed at the development and application, including sensitivity analysis, of a multiyear linear programming model to optimize the financial return and water use, at farm level for Jaíba irrigation scheme, Minas Gerais State, Brazil, using data on crop irrigation requirement and yield, obtained from previous simulation with MCID model. The linear programming model outputted a crop pattern to which a maximum total net present value of R$ 372,723.00 for the four years period, was obtained. Constraints on monthly water availability, labor, land and production were critical in the optimal solution. In relation to the water use optimization, it was verified that an expressive reductions on the irrigation requirements may be achieved by small reductions on the maximum total net present value.

Aging based maintenance and reinvestment scheduling of electric distribution

The maintenance of electric distribution network is a topical question for distribution system operators because of increasing significance of failure costs. In this dissertation the maintenance practices of the distribution system operators are analyzed and a theory for scheduling maintenance activities and reinvestment of distribution components is created. The scheduling is based on the deterioration of components and the increasing failure rates due to aging. The dynamic programming algorithm is used as a solving method to maintenance problem which is caused by the increasing failure rates of the network. The other impacts of network maintenance like environmental and regulation reasons are not included to the scope of this thesis. Further the tree trimming of the corridors and the major disturbance of the network are not included to the problem optimized in this thesis. For optimizing, four dynamic programming models are presented and the models are tested. Programming is made in VBA-language to the computer. For testing two different kinds of test networks are used. Because electric distribution system operators want to operate with bigger component groups, optimal timing for component groups is also analyzed. A maintenance software package is created to apply the presented theories in practice. An overview of the program is presented.

Object-oriented Programming Applied to the Development of Structural Analysis and Optimization Software

This paper presents the development of a two-dimensional interactive software environment for structural analysis and optimization based on object-oriented programming using the C++ language. The main feature of the software is the effective integration of several computational tools into graphical user interfaces implemented in the Windows-98 and Windows-NT operating systems. The interfaces simplify data specification in the simulation and optimization of two-dimensional linear elastic problems. NURBS have been used in the software modules to represent geometric and graphical data. Extensions to the analysis of three-dimensional problems have been implemented and are also discussed in this paper.

Applying Qt to programming courses

Työn tavoitteena on sovittaa Qt opetussuunnitelmaan. Työ sisältää Qt:n lyhyen historian sekä katsauksen sen nykytilaan. Nykytilakatsaus sisältää kolme näkökulmaa: miten ja missä Qt:ta voidaan käyttää, sekä sen käyttötarkoitukset teollisuudessa ja opetuksessa. Työn tuloksena syntyy luentodemonstraatiota varten pieni ohjelma, joka on luotu C++:n ja Qt Designerin avulla ja käyttää olennaisia käyttöliittymäkirjaston olioita. Toisena tuotteena työssä syntyy luonnos Lappeenrannan Teknillisen Yliopiston ohjelmointikursseista, joissa Qt:ta voitaisiin käyttää avustamaan opiskelijoita näkemään, miten graafinen ohjelma luodaan sekä valmentaa heitä ymmärtämään viitekehyksien ja graafisten kirjastojen tuomat edut.

Floristic composition and phytogeography of the tree component of Araucaria Forest fragments in southern Brazil

The present study examined the floristic composition of three fragments of Araucaria Forest (AF) in the Planalto Catarinense region of southern Brazil as well as the floristic contextualization of these areas in relation to other remnant AF sites. Three AF fragments at different altitudes were analyzed in the municipalities of Campos Novos, Lages, and Painel. Fifty 200 m² plots were examined in each fragment and all of the trees with CBH (circumference at breast height) > 15.7 cm were identified. In order to floristically contextualize the study fragments, comparisons were made with other remnant AF sites by way of dendrograms and NMDS (Non-metric multidimensional scaling). Environmental and spatial variables were plotted on the diagram produced by the NMDS to evaluate their influence on the floristic patterns encountered. The forest fragments studied demonstrated high floristic heterogeneity, indicating that AFs cannot be considered homogeneous formations and they could be classified into 3 phytogeographical categories: i) high altitude areas influenced by cloud cover/fog, including the Painel region; ii) areas of lesser altitude and greater mean annual temperatures situated in the Paraná River basin, and iii) areas situated in the Paraná and Upper-Uruguay river basins and the smaller basins draining directly into the southern Atlantic, near Campos Novos and Lages. The environmental variables most highly correlated with species substitutions among the sites were altitude, mean annual temperature, and the mean temperature of the most humid trimester.

Vibrations in Rotating Machinery Arising from Minor Imperfections in Component Geometries

Vibrations in machines can cause noise, decrease the performance, or even damage the machine. Vibrations appear if there is a source of vibration that excites the system. In the worst case scenario, the excitation frequency coincides with the natural frequency of the machine causing resonance. Rotating machines are a machine type, where the excitation arises from the machine itself. The excitation originates from the mass imbalance in the rotating shaft, which always exists in machines that are manufactured using conventional methods. The excitation has a frequency that is dependent on the rotational speed of the machine. The rotating machines in industrial use are usually designed to rotate at a constant rotational speed, the case where the resonances can be easily avoided. However, the machines that have a varying operational speed are more problematic due to a wider range of frequencies that have to be avoided. Vibrations, which frequencies equal to rotational speed frequency of the machine are widely studied and considered in the typical machine design process. This study concentrates on vibrations, which arise from the excitations having frequencies that are multiples of the rotational speed frequency. These vibrations take place when there are two or more excitation components in a revolution of a rotating shaft. The dissertation introduces four studies where three kinds of machines are experiencing vibrations caused by different excitations. The first studied case is a directly driven permanent magnet generator used in a wind power plant. The electromagnetic properties of the generator cause harmonic excitations in the system. The dynamic responses of the generator are studied using the multibody dynamics formulation. In another study, the finite element method is used to study the vibrations of a magnetic gear due to excitations, which frequencies equal to the rotational speed frequency. The objective is to study the effects of manufacturing and assembling inaccuracies. Particularly, the eccentricity of the rotating part with respect to non-rotating part is studied since the eccentric operation causes a force component in the direction of the shortest air gap. The third machine type is a tube roll of a paper machine, which is studied while the tube roll is supported using two different structures. These cases are studied using different formulations. In the first case, the tube roll is supported by spherical roller bearings, which have some wavinesses on the rolling surfaces. Wavinesses cause excitations to the tube roll, which starts to resonate at the frequency that is a half of the first natural frequency. The frequency is in the range where the machine normally operates. The tube roll is modeled using the finite element method and the bearings are modeled as nonlinear forces between the tube roll and the pedestals. In the second case studied, the tube roll is supported by freely rotating discs, which wavinesses are also measured. The above described phenomenon is captured as well in this case, but the simulation methodology is based on the flexible multibody dynamics formulation. The simulation models that are used in both of the last two cases studied are verified by measuring the actual devices and comparing the simulated and measured results. The results show good agreement.

Nonconventional amide bond formation catalysis: programming enzyme specificity with substrate mimetics

This article reports on the design and characteristics of substrate mimetics in protease-catalyzed reactions. Firstly, the basis of protease-catalyzed peptide synthesis and the general advantages of substrate mimetics over common acyl donor components are described. The binding behavior of these artificial substrates and the mechanism of catalysis are further discussed on the basis of hydrolysis, acyl transfer, protein-ligand docking, and molecular dynamics studies on the trypsin model. The general validity of the substrate mimetic concept is illustrated by the expansion of this strategy to trypsin-like, glutamic acid-specific, and hydrophobic amino acid-specific proteases. Finally, opportunities for the combination of the substrate mimetic strategy with the chemical solid-phase peptide synthesis and the use of substrate mimetics for non-peptide organic amide synthesis are presented.

The hemolytic component of cancer anemia: effects of osmotic and metabolic stress on the erythrocytes of rats bearing multifocal inoculations of the Walker 256 tumor

Cancer anemia is classified as an anemia of chronic diseases, although it is sometimes the first symptom of cancer. Cancer anemia includes a hemolytic component, important in the terminal stage when even transfused cells are rapidly destroyed. The presence of a chronic component and the terminal complications of the illness limit studies of the hemolytic component. A multifocal model of tumor growth was used here to simulate the terminal metastatic dissemination stage (several simultaneous inoculations of Walker 256 cells). The hemolytic component of anemia began 3-4 days after inoculation in 100% of the rats and progressed rapidly thereafter: Hb levels dropped from 14.9 ± 0.02 to 8.7 ± 0.06 from days 7 to 11 (~5 times the physiologically normal rate in rats) in the absence of bleeding. The development of anemia was correlated (r2 = 0.86) with the development of other systemic effects such as anorexia. There was a significant decrease in the osmotic fragility of circulating erythrocytes: the NaCl concentration causing 50% lysis was reduced from 4.52 ± 0.06 to 4.10 ± 0.01 (P<0.01) on day 7, indicating a reduction in erythrocyte volume. However, with mild metabolic stress (4-h incubation at 37oC), the erythrocytes showed a greater increase in osmotic fragility than the controls, suggesting marked alteration of erythrocyte homeostasis. These effects may be due to primary plasma membrane alterations (transport and/or permeability) and/or may be secondary to metabolic changes. This multifocal model is adequate for studying the hemolytic component of cancer anemia since it is rapid, highly reproducible and causes minimal animal suffering.

Production and characterization of a monoclonal antibody against an Ascaris suum allergenic component

Ascaris suum allergenic components (PIII) separated by gel filtration chromatography of an adult worm extract were used to immunize BALB/c mice. Popliteal lymph node cells taken from the immunized animals were fused with SP2/O myeloma cells using polyethylene glycol (MW 1450) as fusogen. The hybridomas were cultured in HAT-containing medium and cloned at limiting dilutions. Supernatants from the growing hybrids were screened by ELISA using plates coated with PIII or the A. suum crude extract. The monoclonal antibody obtained, named MAC-3 (mouse anti-A. suum allergenic component), is an IgG1 kappa mouse immunoglobulin that specifically recognizes a 29,000 molecular weight protein (called allergenic protein) with an affinity constant of 1.7 x 10(9) M-1. The A. suum components recognized by MAC-3 induce specific IgE antibody production in immunized BALB/c mice. Ascitic fluid induced in Swiss mice by injecting ip the hybridoma cells and incomplete Freund's adjuvant was purified by affinity chromatography using a protein A-Sepharose column. The purified monoclonal antibody was then coupled to activated Sepharose beads in order to isolate the A. suum allergenic component from the whole extract by affinity chromatography.

Identification and characterization of the two-component NtrY/NtrX regulatory system in Azospirillum brasilense

Two Azospirillum brasilense open reading frames (ORFs) exhibited homology with the two-component NtrY/NtrX regulatory system from Azorhizobium caulinodans. These A. brasilense ORFs, located downstream to the nifR3ntrBC operon, were isolated, sequenced and characterized. The present study suggests that ORF1 and ORF2 correspond to the A. brasilense ntrY and ntrX genes, respectively. The amino acid sequences of A. brasilense NtrY and NtrX proteins showed high similarity to sensor/kinase and regulatory proteins, respectively. Analysis of lacZ transcriptional fusions by the ß-galactosidase assay in Escherichia coli ntrC mutants showed that the NtrY/NtrX proteins failed to activate transcription of the nifA promoter of A. brasilense. The ntrYX operon complemented a nifR3ntrBC deletion mutant of A. brasilense for nitrate-dependent growth, suggesting a possible cross-talk between the NtrY/X and NtrB/C sensor/regulator pairs. Our data support the existence of another two-component regulatory system in A. brasilense, the NtrY/NtrX system, probably involved in the regulation of nitrate assimilation.

Developing an introductory object-oriented programming course

The state of the object-oriented programming course in Lappeenranta University of Technology had reached the point, where it required changes to provide better learning opportunities and thus the learning outcomes. Based on the student feedback the course was partially dated and ineffective. The components of the course were analysed and the ineffective elements were removed and new methods were introduced to improve the course. The major changes included the change from traditional teaching methods to reverse classroom method and the use of Java as the programming language. The changes were measured by the student feedback, lecturer’s observations and comparison to previous years. The feedback suggested that the changes were successful; the course received higher overall grade than before.

Semantic and fuzzy modelling for human behaviour recognition in smart spaces : a case study on ambient assisted living.

Human activity recognition in everyday environments is a critical, but challenging task in Ambient Intelligence applications to achieve proper Ambient Assisted Living, and key challenges still remain to be dealt with to realize robust methods. One of the major limitations of the Ambient Intelligence systems today is the lack of semantic models of those activities on the environment, so that the system can recognize the speci c activity being performed by the user(s) and act accordingly. In this context, this thesis addresses the general problem of knowledge representation in Smart Spaces. The main objective is to develop knowledge-based models, equipped with semantics to learn, infer and monitor human behaviours in Smart Spaces. Moreover, it is easy to recognize that some aspects of this problem have a high degree of uncertainty, and therefore, the developed models must be equipped with mechanisms to manage this type of information. A fuzzy ontology and a semantic hybrid system are presented to allow modelling and recognition of a set of complex real-life scenarios where vagueness and uncertainty are inherent to the human nature of the users that perform it. The handling of uncertain, incomplete and vague data (i.e., missing sensor readings and activity execution variations, since human behaviour is non-deterministic) is approached for the rst time through a fuzzy ontology validated on real-time settings within a hybrid data-driven and knowledgebased architecture. The semantics of activities, sub-activities and real-time object interaction are taken into consideration. The proposed framework consists of two main modules: the low-level sub-activity recognizer and the high-level activity recognizer. The rst module detects sub-activities (i.e., actions or basic activities) that take input data directly from a depth sensor (Kinect). The main contribution of this thesis tackles the second component of the hybrid system, which lays on top of the previous one, in a superior level of abstraction, and acquires the input data from the rst module's output, and executes ontological inference to provide users, activities and their in uence in the environment, with semantics. This component is thus knowledge-based, and a fuzzy ontology was designed to model the high-level activities. Since activity recognition requires context-awareness and the ability to discriminate among activities in di erent environments, the semantic framework allows for modelling common-sense knowledge in the form of a rule-based system that supports expressions close to natural language in the form of fuzzy linguistic labels. The framework advantages have been evaluated with a challenging and new public dataset, CAD-120, achieving an accuracy of 90.1% and 91.1% respectively for low and high-level activities. This entails an improvement over both, entirely data-driven approaches, and merely ontology-based approaches. As an added value, for the system to be su ciently simple and exible to be managed by non-expert users, and thus, facilitate the transfer of research to industry, a development framework composed by a programming toolbox, a hybrid crisp and fuzzy architecture, and graphical models to represent and con gure human behaviour in Smart Spaces, were developed in order to provide the framework with more usability in the nal application. As a result, human behaviour recognition can help assisting people with special needs such as in healthcare, independent elderly living, in remote rehabilitation monitoring, industrial process guideline control, and many other cases. This thesis shows use cases in these areas.