Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code.

Modeling of ALFA Programs Using PVS Theorem Prover

In Safety critical software failure can have a high price. Such software should be free of errors before it is put into operation. Application of formal methods in the Software Development Life Cycle helps to ensure that the software for safety critical missions are ultra reliable. PVS theorem prover, a formal method tool, can be used for the formal verification of software in ADA Language for Flight Software Application (ALFA.). This paper describes the modeling of ALFA programs for PVS theorem prover. An ALFA2PVS translator is developed which automatically converts the software in ALFA to PVS specification. By this approach the software can be verified formally with respect to underflow/overflow errors and divide by zero conditions without the actual execution of the code

The status and barriers to the implementation and continuation of the school gardening projects in Germany, Nigeria and the United States of America

In drawing a conclusion for this study, care must be taken in generalizing findings since the population of students and teachers investigated were limited to certain levels in the different schools and countries. This study recognized some complexity of the factors underlying the status of school gardening instruction and activities in Germany, Nigeria and the U.S. as inadequate time for decision-making in the process of gardening, motivation of teachers and students. This was seen as the major impediments that influenced the status of gardening in the three countries. However, these factors were considered to have affected students’ mode of participation in the school gardening projects. This research finding suggests that the promotion and encouragement of students in gardening activities will promote vegetable production and increasing the numbers of practical farmers. Gardening has the potential to create opportunities for learning in an environment where children are able to experience nature first hand and to use the shared experience for communication (Bowker & Tearle, 2007). Therefore, the need for students to be encouraged to participate in gardening programs as the benefit will not only reduce the rate of obesity currently spreading among youths, but will contribute to the improve knowledge on science subjects. To build a network between community, parents and schools, a parent’s community approach should be used as the curriculum. The community approach will tighten the link between schools; community members, parents, teachers and students. This will help facilitate a better gardening projects implementation. Through a close collaboration, teachers and students will be able to identify issues affecting communities and undertake action learning in collaboration with community organizations to assess community needs and plan the implementation strategies as parents are part of the community. The sense of efficacy is a central factor in motivational and learning processes that govern educational improvement, standard and performance on complex tasks of both teachers and students. Dedication and willingness are the major stimulator and achievement of a project. Through a stimulator and provision of incentives and facilities, schools can achieve the best in project development. Teachers and principals should be aware that students are the lever for achieving the set goals in schools. Failure to understand what students need will result in achieving zero result. Therefore, it is advised that schools focus more on how to lure students to work through proper collaboration with the parents and community members. Principals and teachers should identify areas where students need to be corrected, helping them to correct the problem will enable them be committed in the schools’ programs.

Alternativas al curriculum ordinario : motivación a través de las nuevas tecnologías.

Ofrecer una alternativa al Curriculum Ordinario para el alumnado desmotivado, utilizando las Nuevas Tecnologías como recurso fundamental, con el objeto de lograr los objetivos generales de etapa y la consiguiente titulación.

Comparing european and asian studies : towards the renewal of curriculum programmes. 'Comparación de estudios europeos y asiáticos : hacia la renovación de los programas de estudio'.

Publicación financiada por el Programa Asia-Link de la Comisión Europea. - Notas a pie de página.

A Compilation Strategy for Numerical Programs Based on Partial Evaluation

This work demonstrates how partial evaluation can be put to practical use in the domain of high-performance numerical computation. I have developed a technique for performing partial evaluation by using placeholders to propagate intermediate results. For an important class of numerical programs, a compiler based on this technique improves performance by an order of magnitude over conventional compilation techniques. I show that by eliminating inherently sequential data-structure references, partial evaluation exposes the low-level parallelism inherent in a computation. I have implemented several parallel scheduling and analysis programs that study the tradeoffs involved in the design of an architecture that can effectively utilize this parallelism. I present these results using the 9- body gravitational attraction problem as an example.

Memory Usage Inference for Object-Oriented Programs

We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages. Given a program with size and alias annotations, our inference system will compute the amount of memory required by the methods to execute successfully as well as the amount of memory released when methods return. The obtained analysis results are useful for networked devices with limited computational resources as well as embedded software.

On-the-Fly Maintenance of Series-Parallel Relationships in Fork-Join Multithreaded Programs

A key capability of data-race detectors is to determine whether one thread executes logically in parallel with another or whether the threads must operate in series. This paper provides two algorithms, one serial and one parallel, to maintain series-parallel (SP) relationships "on the fly" for fork-join multithreaded programs. The serial SP-order algorithm runs in O(1) amortized time per operation. In contrast, the previously best algorithm requires a time per operation that is proportional to Tarjan’s functional inverse of Ackermann’s function. SP-order employs an order-maintenance data structure that allows us to implement a more efficient "English-Hebrew" labeling scheme than was used in earlier race detectors, which immediately yields an improved determinacy-race detector. In particular, any fork-join program running in T₁ time on a single processor can be checked on the fly for determinacy races in O(T₁) time. Corresponding improved bounds can also be obtained for more sophisticated data-race detectors, for example, those that use locks. By combining SP-order with Feng and Leiserson’s serial SP-bags algorithm, we obtain a parallel SP-maintenance algorithm, called SP-hybrid. Suppose that a fork-join program has n threads, T₁ work, and a critical-path length of T[subscript ∞]. When executed on P processors, we prove that SP-hybrid runs in O((T₁/P + PT[subscript ∞]) lg n) expected time. To understand this bound, consider that the original program obtains linear speed-up over a 1-processor execution when P = O(T₁/T[subscript ∞]). In contrast, SP-hybrid obtains linear speed-up when P = O(√T₁/T[subscript ∞]), but the work is increased by a factor of O(lg n).

Ciencia, tecnología y sociedad en la enseñanza secundaria : hacia la penetración en el curriculum de los aspectos sociales de la ciencia y tecnología.

Probar mediante el análisis de diferentes materiales didácticos, libros de texto y Cuadernillos Argo, cómo cada uno de ellos responde a una concepción distinta del curriculum. Cinco libros de texto de diferentes editoriales y 7 cuadernillos del Grupo Argo de educación secundaria con contenidos en ciencia, tecnología y sociedad. En la primera parte se realiza una presentación en el ámbito internacional del enfoque Ciencia, Tecnología y Sociedad (CTS) que intenta contextualizar el origen intelectual, académico y educativo de la enseñanza CTS que se desarrolla en España. También se explica cómo se introduce la CTS en el curriculum español y cuáles son algunas de las lineas de trabajo representativas de los programas, y trabajos de investigación CTS en nuestro país. En la segunda parte, se pretende profundizar en las propuestas de enseñanza CTS a través del análisis de materiales didácticos, para terminar con las conclusiones generales. Tablas. La investigación en el curriculum de los aspectos sociales de la Ciencia y Tecnología debe intentar conseguir principalmente dos objetivos: relacionar las dos tradiciones CTS a través de casos de estudio que tengan relevancia social y hacerlo desde una perspectiva social crítica que fundamente los aspectos teóricos. Se debe optar por la investigación de un curriculum integrado en la enseñanza de las relaciones Ciencia, Tecnología y Sociedad en la Educación Secundaria, ya que el carácter interdisciplinar de los estudios CTS hace necesario un planteamiento didáctico coherente. Hay que abordar la investigación en el curriculum desde teorías socioculturales que fundamenten el aprendizaje del alumnado y que al mismo tiempo expliquen la construcción social de la ciencia y la tecnología.

Student self-assessment a feedback seeking strategy through competence evaluation

There is a body of literature that suggests that student self-assessment is a main goal in higher education (Boud et al., 1995; Tan, 2008); moreover new forms of work organization require a high level of skills and competences. The efforts to deal with competence gaps could be developed at many levels, such as employers, educational institutions, individuals and public agents. Employers could put into practice competence development programs to moderate these gaps. Educational institutions can restructure the curriculum to support students in attaining the competences that are essential in the labour market. Individuals themselves may deploy their resources (time and money) in general or specific competence training. Further, government agencies could fund competence promotion programs. Such challenges for education drive change in learning curricula and method, to properly include the competences required for developing global workers who can move beyond basic competence, to enhanced flexibility and adaptability. In performance assessment methods, there is a shift from the traditional exam-based assessments to more innovative task assessment, which considers performance in multiple different tasks carry out by students. ICTs make it technologically feasible to carry out a complete and complex selfassessment of competences, which provides immediate results to students or other recipients. In the case of students, the evaluation of competences is relevant as developing competences is part - if not all - of the objectives of education. Therefore, it is an important element of the quality of educational organizations (e.g., universities), and of their organizational success. Further, educational organizations may put special emphasis on some differentiating competences, which can be a means of positioning and differentiation from competitors. Competence assessment is an instrument to make students conscious of their strengths and weaknesses, leading to higher motivation to develop their own learning career

Implementation of training programs in self-regulated learning strategies in Moodle format : Results of a experience in higher education

Resumen tomado de la publicaci??n