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.

Memristive Computing

Memristive computing refers to the utilization of the memristor, the fourth fundamental passive circuit element, in computational tasks. The existence of the memristor was theoretically predicted in 1971 by Leon O. Chua, but experimentally validated only in 2008 by HP Labs. A memristor is essentially a nonvolatile nanoscale programmable resistor — indeed, memory resistor — whose resistance, or memristance to be precise, is changed by applying a voltage across, or current through, the device. Memristive computing is a new area of research, and many of its fundamental questions still remain open. For example, it is yet unclear which applications would benefit the most from the inherent nonlinear dynamics of memristors. In any case, these dynamics should be exploited to allow memristors to perform computation in a natural way instead of attempting to emulate existing technologies such as CMOS logic. Examples of such methods of computation presented in this thesis are memristive stateful logic operations, memristive multiplication based on the translinear principle, and the exploitation of nonlinear dynamics to construct chaotic memristive circuits. This thesis considers memristive computing at various levels of abstraction. The first part of the thesis analyses the physical properties and the current-voltage behaviour of a single device. The middle part presents memristor programming methods, and describes microcircuits for logic and analog operations. The final chapters discuss memristive computing in largescale applications. In particular, cellular neural networks, and associative memory architectures are proposed as applications that significantly benefit from memristive implementation. The work presents several new results on memristor modeling and programming, memristive logic, analog arithmetic operations on memristors, and applications of memristors. The main conclusion of this thesis is that memristive computing will be advantageous in large-scale, highly parallel mixed-mode processing architectures. This can be justified by the following two arguments. First, since processing can be performed directly within memristive memory architectures, the required circuitry, processing time, and possibly also power consumption can be reduced compared to a conventional CMOS implementation. Second, intrachip communication can be naturally implemented by a memristive crossbar structure.

Geometric nonlinear dynamic analysis of plates and shells using eight-node hexahedral finite elements with reduced integration

This work presents a geometric nonlinear dynamic analysis of plates and shells using eight-node hexahedral isoparametric elements. The main features of the present formulation are: (a) the element matrices are obtained using reduced integrations with hourglass control; (b) an explicit Taylor-Galerkin scheme is used to carry out the dynamic analysis, solving the corresponding equations of motion in terms of velocity components; (c) the Truesdell stress rate tensor is used; (d) the vector processor facilities existing in modern supercomputers were used. The results obtained are comparable with previous solutions in terms of accuracy and computational performance.

Multiple scales analysis of nonlinear oscillations of a portal frame foundation for several machines

An analytical study of the nonlinear vibrations of a multiple machines portal frame foundation is presented. Two unbalanced rotating machines are considered, none of them resonant with the lower natural frequencies of the supporting structure. Their combined frequencies is set in such a way as to excite, due to nonlinear behavior of the frame, either the first anti-symmetrical mode (sway) or the first symmetrical mode. The physical and geometrical characteristics of the frame are chosen to tune the natural frequencies of these two modes into a 1:2 internal resonance. The problem is reduced to a two degrees of freedom model and its nonlinear equations of motions are derived via a Lagrangian approach. Asymptotic perturbation solutions of these equations are obtained via the Multiple Scales Method.

Effect of wave frequency on the nonlinear interaction between Görtler vortices and three-dimensional Tollmien-Schlichting waves

The nonlinear interaction between Görtler vortices (GV) and three-dimensional Tollmien-Schlichting (TS) waves nonlinear interaction is studied with a spatial, nonparallel model based on the Parabolized Stability Equations (PSE). In this investigation the effect of TS wave frequency on the nonlinear interaction is studied. As verified in previous investigations using the same numerical model, the relative amplitudes and growth rates are the dominant parameters in GV/TS wave interaction. In this sense, the wave frequency influence is important in defining the streamwise distance traveled by the disturbances in the unstable region of the stability diagram and in defining the amplification rates that they go through.

Development of a three-dimensional nonlinear viscoelastic constitutive model of solid propellant

A three dimensional nonlinear viscoelastic constitutive model for the solid propellant is developed. In their earlier work, the authors have developed an isotropic constitutive model and verified it for one dimensional case. In the present work, the validity of the model is extended to three-dimensional cases. Large deformation, dewetting and cyclic loading effects are treated as the main sources of nonlinear behavior of the solid propellant. Viscoelastic dewetting criteria is used and the softening of the solid propellant due to dewetting is treated by the modulus decrease. The nonlinearities during cyclic loading are accounted for by the functions of the octahedral shear strain measure. The constitutive equation is implemented into a finite element code for the analysis of propellant grains. A commercial finite element package ‘ABAQUS’ is used for the analysis and the model is introduced into the code through a user subroutine. The model is evaluated with different loading conditions and the predicted values are in good agreement with the measured ones. The resulting model applied to analyze a solid propellant grain for the thermal cycling load.

Nonlinear dynamics and control of multibody systems

The dynamics of flexible systems, such as robot manipulators , mechanical chains or multibody systems in general, is becoming increasingly important in engineering. This article deals with some nonlinearities that arise in the study of dynamics and control of multibody systems in connection to large rotations. Specifically, a numerical scheme that adresses the conservation of fundamental constants is presented in order to analyse the control-structure interaction problems.

A frequency-domain pseudo-force method for dynamic structural analysis nonlinear systems and nonproportional damping

A frequency-domain method for nonlinear analysis of structural systems with viscous, hysteretic, nonproportional and frequency-dependent damping is presented. The nonlinear effects and nonproportional damping are considered through pseudo-force terms. The modal coordinates uncoupled equations are iteratively solved. The treatment of initial conditions in the frequency domain which is necessary for the treatment of the uncoupled equations is initially adressed.

On the numerical integration of rigid body nonlinear dynamics in presence of parameters singularities

One of the main complexities in the simulation of the nonlinear dynamics of rigid bodies consists in describing properly the finite rotations that they may undergo. It is well known that, to avoid singularities in the representation of the SO(3) rotation group, at least four parameters must be used. However, it is computationally expensive to use a four-parameters representation since, as only three of the parameters are independent, one needs to introduce constraint equations in the model, leading to differential-algebraic equations instead of ordinary differential ones. Three-parameter representations are numerically more efficient. Therefore, the objective of this paper is to evaluate numerically the influence of the parametrization and its singularities on the simulation of the dynamics of a rigid body. This is done through the analysis of a heavy top with a fixed point, using two three-parameter systems, Euler's angles and rotation vector. Theoretical results were used to guide the numerical simulation and to assure that all possible cases were analyzed. The two parametrizations were compared using several integrators. The results show that Euler's angles lead to faster integration compared to the rotation vector. An Euler's angles singular case, where representation approaches a theoretical singular point, was analyzed in detail. It is shown that on the contrary of what may be expected, 1) the numerical integration is very efficient, even more than for any other case, and 2) in spite of the uncertainty on the Euler's angles themselves, the body motion is well represented.

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.

Covalidation of Integral Transforms and Method of Lines in Nonlinear Convection-Diffusion with Mathematica

The Mathematica system (version 4.0) is employed in the solution of nonlinear difusion and convection-difusion problems, formulated as transient one-dimensional partial diferential equations with potential dependent equation coefficients. The Generalized Integral Transform Technique (GITT) is first implemented for the hybrid numerical-analytical solution of such classes of problems, through the symbolic integral transformation and elimination of the space variable, followed by the utilization of the built-in Mathematica function NDSolve for handling the resulting transformed ODE system. This approach ofers an error-controlled final numerical solution, through the simultaneous control of local errors in this reliable ODE's solver and of the proposed eigenfunction expansion truncation order. For covalidation purposes, the same built-in function NDSolve is employed in the direct solution of these partial diferential equations, as made possible by the algorithms implemented in Mathematica (versions 3.0 and up), based on application of the method of lines. Various numerical experiments are performed and relative merits of each approach are critically pointed out.

Estimating Attractor Dimension on the Nonlinear Pendulum Time Series

Chaotic dynamical systems exhibit trajectories in their phase space that converges to a strange attractor. The strangeness of the chaotic attractor is associated with its dimension in which instance it is described by a noninteger dimension. This contribution presents an overview of the main definitions of dimension discussing their evaluation from time series employing the correlation and the generalized dimension. The investigation is applied to the nonlinear pendulum where signals are generated by numerical integration of the mathematical model, selecting a single variable of the system as a time series. In order to simulate experimental data sets, a random noise is introduced in the time series. State space reconstruction and the determination of attractor dimensions are carried out regarding periodic and chaotic signals. Results obtained from time series analyses are compared with a reference value obtained from the analysis of mathematical model, estimating noise sensitivity. This procedure allows one to identify the best techniques to be applied in the analysis of experimental data.