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

Evaluaci??n y acci??n tutorial en educaci??n primaria

Se presenta experiencia educativa que propone elaborar el proyecto curricular del centro para adaptarlo a las necesidades reales del contexto. Se realiza en el CEIP Cristo de la Salud en N??var, Granada. Los objetivos son: desarrollar los apartados del proyecto curricular del centro; elaborar los elementos del proyecto curricular de centro; evaluaci??n del proyecto curricular.

Psicopedagogía de la función tutorial y orientación.

La obra es el resultado de la publicación de los materiales del curso de Psicopedagogía de la función tutorial y orientación del Programa de Formación del Profesorado conveniado entre el sindicato ANPE y el MEC. El curso se compone de once unidades didácticas divididas en cinco bloques de contenidos. El primero trata de cuestiones generales sobre psicología evolutiva de los alumnos en las etapas de educación infantil, primaria y secundaria, además de la legislación aplicable. En el segundo se sitúa la orientación en el marco de la nueva ordenación general del sistema educativo; en el tercero se aborda la acción tutorial y a la diversidad y dinámicas de grupo se dedican los últimos bloques.

Propuesta de plan de acción tutorial.

El proyecto trata de la elaboración de un plan de actuación del departamento de orientación, concretamente de la elaboración de un plan tutorial, incardinado en la programación general anual en lo que afecta al mencionado departamento. Los bloques de contenido propuestos para la acción tutorial son: convivir, aprender, evaluar, ser persona y tomar decisiones.

La orientación y la acción tutorial en el sistema educativo.

Materiales de un curso de formación de profesorado organizado por el sindicato ANPE y titulado: La orientación tutorial en el sistema educativo, compuesto por catorce unidades didácticas que completan y amplían los materiales de una edición anterior titulada: Psicopedagogía de la función tutorial y orientación. Entre otros los temas abordados son: dinámica de grupos, legislación sobre orientación y tutoría, evolutiva de los alumnos de infantil, primaria y ESO, la acción tutorial, funciones del tutor, líneas de actuación, atención a la diversidad y la acción tutorial en Bachillerato y F.P. específica.

La acción tutorial en primaria.

Proyecto tutorial dirigido a los profesores de primaria cuyo objetivo es integrar la tutoría en la práctica formativa. El libro consta de dos partes, la primera, en la que se aborda la acción tutorial como ámbito de la orientación educativa presente en los proyectos de centro y propone y ejemplifica un Plan de Acción Tutorial y la segunda, compuesta íntegramente por actividades tutoriales en los diferentes ámbitos de trabajo en los centros de primaria.

Sistematización de la función tutorial en secundaria.

El libro está elaborado a modo de catálogo de experiencias y actividades planificadas que abordan los temas fundamentales de la función tutorial

La orientación y la acción tutorial en el sistema educativo : fundamentos teóricos y legislativos.

El manual contiene una sección de páginas web relacionadas con la temática tratada y un glosario para la mejor comprensión de la misma

La orientación y la acción tutorial en el sistema educativo : aspectos psicoevolutivos y niveles de organización escolar.

El manual contiene una sección de páginas web relacionadas con la temática tratada y un glosario para la mejor comprensión de la misma. - Parte de la bibliografía está comentada

La orientaci??n y la acci??n tutorial en el sistema educativo : la tutor??a, l??neas de actuaci??n tutorial y atenci??n a la diversidad

En anexo figura un documento-tipo de adaptaci??n curricular, una relaci??n de p??ginas web sobre el tema y un glosario de t??rminos.

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).

Pla d'acció tutorial de la Facultat de Ciències de la UdG

En aquest article es presenta el Pla d’Acció Tutorial (PAT) per als alumnes de primer curs dels tres estudis de la Facultat de Ciències de la UdG, Biologia, Química i Ciències Ambientals, implantat en el marc del plans pilot de la UdG a partir del curs 2007. El PAT proposa treballar una sèrie de competències transversals entre les que destaca ’Responsabilitzar l’estudiant del seu procés d’aprenentatge’. S’assigna un tutor per un grup de 15 alumnes, s’estableixen tutories generals i concertades (3 alumnes), s’elaboren una agenda i un seguit d’enquestes per tal de realitzar el seguiment dels alumnes, es proposa als alumnes un espai de reflexió i s’avalua la progressió en la consecució de la competència. Finalment es fa un seguiment tant de les opinions dels tutors com dels alumnes tutoritzats en relació al PAT