Search

The main aim of this paper work is to analyze the conceptions that the college students have about learning in their process of training as teachers. A questionnaire to 145 students from the University of Seville was administered. 102 in their first semester of the education undergraduate program and 43 in the second cycle of their courses. Answers to the question "what would you say learning is?" have been analyzed using an ad hoc category system based on four criteria with two levels of complexity each: a) Persons involved; B) Role of the student; C) Functionality; and d) Transformational dimension of learning. The data show that in all the criteria there are proportionally more responses included in the less complex condition. Thus, in the criterion 'people involved in the learning process', 88.8% refer only to the participation of the learner in the learning process, and 11.2% refer to the learner's participation and somebody else. In the criterion 'role of the student', 74.8% of them refer to the passive role of the student, while only 25.2% refer to an active-constructive role. Only 24.5% of students do not allude to the 'learning functionality' and only the 9.1% of participant refer explicitly to the 'transformational dimension'. When comparing the two groups of the sample, first and last year students, significant differences in three of the four criteria are found. These results are consistent with other researches that have studied the conceptions about learning. Reflections and ideas into the training received by the students of education undergraduate program are presented, since after four years of university experience they do not surpass, for the most part, quantitative, realistic and reproductive conceptions of learning.

Las concepciones actuales sobre enseñanza y aprendizaje y las actuaciones educativas que se basan en ellas sitúan la clave del aprendizaje en las interacciones que se producen en los espacios educativos destacando la necesidad de incrementar la cantidad, diversidad y calidad de dichas interacciones como condición para mejorar el aprendizaje. Con esa finalidad, en este trabajo se proponen una serie de criterios que optimizan la calidad de las interacciones y caracterizan el estilo de interacción dialógica del profesorado. Para identificarlos se analizaron las videograbaciones de 26 sesiones de situaciones de interacción de diferentes docentes de Educación Especial y Educación Primaria cuyo alumnado habían obtenido diferentes resultados en pruebas de desarrollo cognitivo tras la implementación del programa de mejora de las habilidades de pensamiento denominado “Comprender y Transformar”. El análisis realizado proporcionó unas pautas repetidas de interacción que se daban entre los grupos de mayores ganancias y que aparecían poco o nada en los demás. Son los Patrones de Movilización Cognitiva (PMC), que constituyen un conjunto sistemático de pautas para la interacción dialógica que puede usarse tanto para el análisis de las interacciones como para la formación del profesorado en los criterios que definen la enseñanza interactiva y dialógica. The current conceptions of teaching and learning and the educational actions based thereon place the key to learning in the interactions that take place in educational spaces, highlighting the need to increase the quantity, diversity, and quality of these interactions as a condition to improve learning. With this purpose, this paper proposes a series of criteria that optimizes the quality of the interactions and characterizes the dialogical interaction style of the teaching staff. To identify these guidelines for dialogical interaction, video recordings of 26 sessions of interaction situations of different Special Education and Primary Education teachers whose students had obtained different results of cognitive development tests after the implementation of a program of improvement of thinking skills, were analysed, called “Understanding and Transforming". These are Cognitive Mobilizing Patterns (CMP), which constitute a systematic set of guidelines for dialogic interaction that may be used for both the analysis of interactions and for teacher training in the criteria that define interactive and dialogical teaching.

This paper presents a decision support system (DSS) based on formal methods for the management of complex river basins in flood scenarios. The DSS is the result of integrating two different DSSs: first, a DSS for dam management that uses the Spin model checker to produce the manoeuvres and the discharged water over time to satisfy user-defined constraints; second, a DSS that performs numeric simulations of rainfall and water flow along the river basin, taking into account the water discharged by dams. By integrating these two DSSs, the user can define constraints over the parameters of the river basin and all the dams. We use Spin to find the sequences of dam manoeuvres that mitigate the effect of floods along the river basin, according to these constraints. This work is part of the SAID project, a European demonstration project whose main goal is to smartly manage river basins by means of the integration of different DSSs. The demonstrator basin is the Guadalhorce river basin, located in the south of Spain. We apply the method to develop a DSS for this river basin in particular, but the approach is general enough that it can be applied to any river basin.

El objetivo de este trabajo es analizar las concepciones de los universitarios, en proceso de formación como docentes, acerca del aprendizaje. Se administró un cuestionario a 145 estudiantes de la Universidad de Sevilla. 102 cursaban primero de Magisterio y 43 Psicopedagogía (segundo ciclo). Las respuestas a la pregunta ¿qué dirías que es aprender? se analizaron mediante un sistema de categorías ad hoc basado en cuatro criterios con dos niveles de complejidad cada uno: a) Personas implicadas; b) Papel del estudiante; c) Funcionalidad; y d) Dimensión transformacional del aprendizaje. Los datos muestran que en todos los criterios existen proporcionalmente más respuestas que se incluyen en el valor menos complejo. Así, en el criterio ‘personas implicadas en el proceso de aprendizaje’, un 88.8% se refieren sólo a la participación del aprendiz en el proceso de aprendizaje, y un 11.2% añaden la participación de otro/s. En el criterio ‘papel del alumno”, un 74.8% refieren el papel pasivo del estudiantado, mientras que sólo un 25.2% aluden al papel activoconstructivo. En cuanto a la ‘funcionalidad del aprendizaje’ sólo un 24.5% se refieren explícitamente a la misma. En relación a la ‘dimensión transformacional’, tan sólo el 9.1% la refieren. Al comparar los dos grupos de la muestra, se encuentran diferencias significativas en tres de los cuatro criterios. Estos resultados son coherentes con otras investigaciones similares y obligan a reflexionar sobre la formación recibida por los estudiantes de Educación, pues tras cuatro años de formación no superan, en su mayoría, concepciones cuantitativas, realistas y reproductivas del aprendizaje., The main aim of this paper work is to analyze the conceptions that the college students have about learning in their process of training as teachers. A questionnaire to 145 students from the University of Seville was administered. 102 in their first semester of the education undergraduate program and 43 in the second cycle of their courses. Answers to the question "what would you say learning is?" have been analyzed using an ad hoc category system based on four criteria with two levels of complexity each: a) Persons involved; B) Role of the student; C) Functionality; and d) Transformational dimension of learning. The data show that in all the criteria there are proportionally more responses included in the less complex condition. Thus, in the criterion 'people involved in the learning process', 88.8% refer only to the participation of the learner in the learning process, and 11.2% refer to the learner's participation and somebody else. In the criterion 'role of the student', 74.8% of them refer to the passive role of the student, while only 25.2% refer to an active-constructive role. Only 24.5% of students do not allude to the 'learning functionality' and only the 9.1% of participant refer explicitly to the 'transformational dimension'. When comparing the two groups of the sample, first and last year students, significant differences in three of the four criteria are found. These results are consistent with other researches that have studied the conceptions about learning. Reflections and ideas into the training received by the students of education undergraduate program are presented, since after four years of university experience they do not surpass, for the most part, quantitative, realistic and reproductive conceptions of learning.

El objetivo de este trabajo es presentar las valoraciones que los estudiantes universitarios, que han participado como voluntarios en centros constituidos como Comunidad de Aprendizaje, hacende su experiencia en Grupos Interactivos.Para la recogida de información pedimos a los participantes que entregaran una memoria con sus valoraciones. En el análisis de dichos informes se ha utilizado una metodología cualitativa basada en análisis del contenido.Los resultados se han agrupado en cinco bloques: Para qué les ha servido colaborar en el voluntariado de grupos interactivos, cómo se han sentido durante esta colaboración, los aspectos positivos que quieren destacar de esta experiencia, los aspectos negativos de la misma y por último las propuestas de mejora que quieran formular.Finalizamos el trabajo señalando que los aspectos positivos sobrepasan con creces a los aspectos negativos y superan ampliamente sus expectativas iniciales tanto a nivel personal como profesional. Por otra parte los resultados confirman en la práctica los siete principios del aprendizaje dialógico sobre el que se sustenta este modelo de actuación educativa.

Las concepciones actuales sobre enseñanza y aprendizaje y las actuaciones educativas que se basan en ellas sitúan la clave del aprendizaje en las interacciones que se producen en los espacios educativos destacando la necesidad de incrementar la cantidad, diversidad y calidad de dichas interacciones como condición para mejorar el aprendizaje. Con esa finalidad, en este trabajo se proponen una serie de criterios que optimizan la calidad de las interacciones y caracterizan el estilo de interacción dialógica del profesorado. Para identificarlos se analizaron las videograbaciones de 26 sesiones de situaciones de interacción de diferentes docentes de Educación Especial y Educación Primaria cuyo alumnado habían obtenido diferentes resultados en pruebas de desarrollo cognitivo tras la implementación del programa de mejora de las habilidades de pensamiento denominado “Comprender y Transformar”. El análisis realizado proporcionó unas pautas repetidas de interacción que se daban entre los grupos de mayores ganancias y que aparecían poco o nada en los demás. Son los Patrones de Movilización Cognitiva (PMC), que constituyen un conjunto sistemático de pautas para la interacción dialógica que puede usarse tanto para el análisis de las interacciones como para la formación del profesorado en los criterios que definen la enseñanza interactiva y dialógica. The current conceptions of teaching and learning and the educational actions based thereon place the key to learning in the interactions that take place in educational spaces, highlighting the need to increase the quantity, diversity, and quality of these interactions as a condition to improve learning. With this purpose, this paper proposes a series of criteria that optimizes the quality of the interactions and characterizes the dialogical interaction style of the teaching staff. To identify these guidelines for dialogical interaction, video recordings of 26 sessions of interaction situations of different Special Education and Primary Education teachers whose students had obtained different results of cognitive development tests after the implementation of a program of improvement of thinking skills, were analysed, called “Understanding and Transforming". These are Cognitive Mobilizing Patterns (CMP), which constitute a systematic set of guidelines for dialogic interaction that may be used for both the analysis of interactions and for teacher training in the criteria that define interactive and dialogical teaching.

En este trabajo se presentan las valoraciones de los y las estudiantes universitarios que han participado como voluntarios en centros constituidos como Comunidad de Aprendizaje. Se ha realizado un análisis del contenido de 23 informes entregados por otros tantos alumnos y alumnas de la titulación de Psicología de la Universidad de Sevilla. Los resultados se han agrupado en cinco bloques que hacen referencia a: a) para qué les ha servido colaborar en el voluntariado; b) cómo se han sentido durante esta colaboración; c) los aspectos positivos que quieren destacar de esta experiencia, d) los aspectos negativos de la misma y por último e) las propuestas de mejora que quieran formular. La principal conclusión de este trabajo es que, a juicio de los participantes, esta experiencia les ha aportado muchos beneficios a nivel profesional y personal, siendo una práctica formativa que valoran muy positivamente y que no sólo recomendarían a otros compañeros y compañeras sino que volverían a repetir. This paper presents the assessment of the voluntary students who have participated in centers established as Learning Community. We have carried out a content analysis of 23 reports of students of the degree in psychology from the University of Sevilla. The results have been grouped into five blocks that refer to: a) what benefit have they obtained from collaborating in the voluntary service; b) how have they felt during the collaboration; c) what are the positive aspects that they would like to highlight from the experience; d) what are the negative aspects of the experience and, lastly; e) improvement proposals that they would like to put forward. The main conclusion of this paper is that, in the view of its participants, this experience has brought them many benefits both at professional and personal levels, being a highly positively valued practice that they would recommend to others colleagues and they would repeat.

Una de las actuaciones educativas de éxito destacada por la investigación más reciente (Includ-ed Consortium, 2011) es la participación y formación de las familias de los escolares y otros miembros de la comunidad que colaboran en los centros educativos. Un modo de concretar dicha formación en Comunidades de Aprendizaje es mediante la realización de tertulias dialógicas en las que participan junto con el profesorado del centro. Aunque es relativamente frecuente encontrar publicaciones que informan de cómo la formación de los familiares repercute en la mejora del aprendizaje escolar, no lo es tanto encontrar referencias que den cuenta de los beneficios que las tertulias dialógicas proporcionan a otro tipo de voluntariado. Con este trabajo pretendemos contribuir a rellenar esa laguna de modo que su objetivo es determinar las percepciones del alumnado universitario colaborador en Comunidades de Aprendizaje acerca del impacto que para ellos ha tenido su participación en tertulias dialógicas. Mediante una metodología cualitativa basada en el análisis del discurso, presentamos la valoración que hacen de las tertulias dialógicas 23 estudiantes de psicología que han participado en ellas, así como los beneficios que dicen haber obtenido de dicha participación. En sus aportaciones, los estudiantes destacan numerosos aspectos positivos (90,36% de las aportaciones), tanto referidos a las tertulias dialógicas como a su participación en ellas confirmando lo que dice al respecto la literatura científica y la experiencia de otros centros que implementan las actuaciones educativas de éxito en la mejora del rendimiento y la superación de los problemas de convivencia. One of the educational actions of success highlighted by the most recent research (Includ-ed Consortium, 2011) is the participation and training of the families of schoolchildren and other members of the community who work in schools. One way to realize such training in Learning Communities is through dialogic gatherings in which they participate together with the teachers of the schools. Although it is relatively common to find publications that inform how the formation of the families it has an impact on the improvement of school learning, not so much find references that realize the benefits that the dialogic gatherings provide another type of volunteering. In this paper we contribute to fill this gap so that its objective is to determine the perceptions of university students contributors in Learning Communities about the impact that they have had their participation in dialogic gatherings. Using a qualitative methodology based on the analysis of the discourse, in this article we present the assessment that the dialogic gatherings make 23 psychology students who have participated in them, as well as the benefits that they say have obtained of such participation. In their contributions, the students highlight many positive aspects (90,36% of the contributions), both referred to the dialogic gatherings as to his participation in them, confirming what he says regarding the scientific literature and the experience of other centres that implement educational practices of success in improving performance and overcoming the problems of coexistence.

This paper presents the foundations and the real use of a tool to automatically detect anomalies in Internet traffic produced by mobile applications. In particular, our MVE tool is focused on analyzing the impact that user interactions have on the traffic produced and received by the smartphones. To make the analysis exhaustive with regard to the potential user behaviors, we follow a model-based approach to automatically generate test cases to be executed on the smartphones. In addition, we make use of a specification language to define traffic patterns to be compared with the actual traffic in the device. MVE also includes monitoring and verification support to detect executions that do not fit the patterns. In these cases, the developer will obtain detailed information on the user actions that produce the anomaly in order to improve the application. To validate the approach, the paper presents an experimental study with the well-known Spotify app for Android, in which we detected some interesting behaviors. For instance, some HTTP connections do not end successfully due to timeout errors from the remote Spotify service.

This paper presents an approach for the automated debugging of reactive and concurrent Java programs, combining model checking and runtime monitoring. Runtime monitoring is used to transform the Java execution traces into the input for the model checker, the purpose of which is twofold. First, it checks these execution traces against properties written in linear temporal logic (LTL), which represent desirable or undesirable behaviors. Second, it produces several execution traces for a single Java program by generating test inputs and exploring different schedulings in multithreaded programs. As state explosion is the main drawback to model checking, we propose two abstraction approaches to reduce the memory requirements when storing Java states. We also present the formal framework to clarify which kinds of LTL safety and liveness formulas can be correctly analysed with each abstraction for both finite and infinite program executions. A major advantage of our approach comes from the model checker, which stores the trace of each failed execution, allowing the programmer to replay these executions to locate the bugs. Our current implementation, the tool TJT, uses Spin as the model checker and the Java Debug Interface (JDI) for runtime monitoring. TJT is presented as an Eclipse plug-in and it has been successfully applied to debug complex public Java programs.

Este trabajo se plantea en el marco del proyecto Teon XXI sobre uso de las TIC aplicadas a la coeducación. En este contexto nuestro objetivo es la elaboración de una escala observacional para evaluar buenas prácticas coeducativas, que sirva de complemento a las metodologías cualitativas habitualmente utilizadas. El instrumento se compone de cinco criterios o indicadores de calidad (eficacia, efecto transformador, sostenibilidad, legitimidad, replicabilidad) definidos en base a conceptos clave que articulan una graduación a intervalos oscilante entre 0 y 4. Los resultados de la aplicación por cuatro jueces a diez prácticas seleccionadas de centros escolares andaluces por su relevancia coeducativa mostraron su adecuada fiabilidad. Concluimos la conveniencia del proceso mismo de construcción de este tipo de escalas como vehículo para la reflexión sobre el concepto de buena práctica, dada su multidimensionalidad y complejidad de definición. Asimismo, se recomienda el análisis desagregado de los distintos criterios para su evaluación. This study is based on the framework of project Teon XXI. The aim of the project was to research the use of ICT in the field of coeducation. In this context our aim is to develop an observational scale to assess coeducational best practices. We consider this evaluation compatible with qualitative methodologies commonly used by our research group. The instrument consists of five criteria or indicators of quality (effectiveness, transformative effect, sustainability, legitimacy, replicability) defined based on key concepts that articulate a graduation between 0 and 4. Four judges assess 10 coeducation’s practices in Andalucía, selected for their significance, using the scale. The results showed an adequate reliability. We conclude the convenience of the constructive process of such scales as a means for reflection on the concept of best practice, its multidimensionality and complexity of definition. We also recommend the disaggregated analysis of the different criteria for evaluation.

El objetivo de este trabajo es presentar las valoraciones que los estudiantes universitarios, que han participado como voluntarios en centros constituidos como Comunidad de Aprendizaje, hacen de su experiencia en Grupos Interactivos. Para la recogida de información pedimos a los participantes que entregaran una memoria con sus valoraciones. En el análisis de dichos informes se ha utilizado una metodología cualitativa basada en análisis del contenido. Los resultados se han agrupado en cinco bloques: Para qué les ha servido colaborar en el voluntariado de grupos interactivos, cómo se han sentido durante esta colaboración, los aspectos positivos que quieren destacar de esta experiencia, los aspectos negativos de la misma y por último las propuestas de mejora que quieran formular. Finalizamos el trabajo señalando que los aspectos positivos sobrepasan con creces a los aspectos negativos y superan ampliamente sus expectativas iniciales tanto a nivel personal como profesional. Por otra parte los resultados confirman en la práctica los siete principios del aprendizaje dialógico sobre el que se sustenta este modelo de actuación educativa., The aim of this article is to present evaluations by university students, who participated as volunteers in centres established as Learning Communities, on their experience in Interactive Groups. In order to collect the information, we asked the participants to hand in a report containing their evaluations. A qualitative methodology based on content analysis was used to examine these reports. The results were grouped into the following five blocks: what use volunteering in an interactive group has been to them, how they felt during the collaboration, positive aspects of the experience they wished to highlight, the negative aspects of it, and, finally, their proposals for improvement. We end this article by pointing out that the positive aspects far outnumber the negative aspects and also far exceed their initial expectations on both personal and professional levels. Furthermore, the results confirm the practical part of the seven principles of dialogic learning on which this educational action model is based, Universidad de Granada. Departamento de Didáctica y Organización Escolar. Grupo FORCE (HUM-386)

Este trabajo está sustentado en los principios y estrategias metodológicas desarrolladas por la psicología cultural, las perspectivas constructivistas, el análisis del discurso y el análisis conversacional. De acuerdo con dicho marco teórico-metodológico este trabajo se centra en el análisis de las prácticas discursivas, los dispositivos, estrategias y recursos comunicativos que utilizan los/las profesores/as y los/las alumnos/as en las aulas. En concreto en este artículo se analizan las formas en la que los participantes del aula (profesores/ as y alumnos/as) se comunican entre sí y captan la atención del «otro» para «convencerlos» de la «verdad» de sus argumentaciones. De entre las diversas formas en que es posible legitimar aquello que se enuncia, nos centraremos en un recurso concreto, las invocaciones. Estas constituirán el objeto de análisis y el punto de partida de este trabajo. Los resultados se fundamentan en el análisis llevado a cabo sobre el desarrollo de dos unidades didácticas en dos aulas universitarias. En el mismo se encuentran dos grandes tipos de invocaciones, aquellas que aluden al conocimiento o autoridades académicas y las que recurren a un conocimiento experiencial. Se presentan, además, ejemplos de fragmentos discursivos en los que se ilustra el uso que hacen profesores y alumnos de tales tipos de invocaciones. Para terminar se exponen algunas de las ventajas de este tipo de análisis. The present survey is based on the principles and methodological strategies developed by cultural psychology, constructivist perspectives, the discourse analysis and conversational analysis. Within that theoretical and methodological framework, this paper focuses on the analysis of discursive practices, devices, communication strategies and the resources which teachers and students use in their classrooms. Specifically, the present article analyzes how classroom participants (teachers and students) communicate and capture the attention of others to "convince» them about the "truth" of their arguments. Among the various likely methods to legitimize what is being stated, this paper focuses on a specific resource: invocations. These are the aim of the analysis and the starting point for this survey. Our results are based on the analysis undertaken through the development of two didactic units in two university classrooms. There are two types of invocations, those referred to academic knowledge or academic authorities and those related to the invocations which use experiential knowledge. In addition, this paper presents some examples of discourse fragments utilized to illustrate how both professors and students use invocations to validate their statements. Finally, some of the advantages of that type of analysis are presented herein.

El objetivo de este trabajo es presentar las valoraciones que los estudiantes universitarios, que han participado como voluntarios en centros constituidos como Comunidad de Aprendizaje, hacen de su experiencia en Grupos Interactivos. Para la recogida de información pedimos a los participantes que entregaran una memoria con sus valoraciones. En el análisis de dichos informes se ha utilizado una metodología cualitativa basada en análisis del contenido. Los resultados se han agrupado en cinco bloques: Para qué les ha servido colaborar en el voluntariado de grupos interactivos, cómo se han sentido durante esta colaboración, los aspectos positivos que quieren destacar de esta experiencia, los aspectos negativos de la misma y por último las propuestas de mejora que quieran formular. Finalizamos el trabajo señalando que los aspectos positivos sobrepasan con creces a los aspectos negativos y superan ampliamente sus expectativas iniciales tanto a nivel personal como profesional. Por otra parte los resultados confirman en la práctica los siete principios del aprendizaje dialógico sobre el que se sustenta este modelo de actuación educativa. The aim of this article is to present evaluations by university students, who participated as volunteers in centres established as Learning Communities, on their experience in Interactive Groups. In order to collect the information, we asked the participants to hand in a report containing their evaluations. A qualitative methodology based on content analysis was used to examine these reports. The results were grouped into the following five blocks: what use volunteering in an interactive group has been to them, how they felt during the collaboration, positive aspects of the experience they wished to highlight, the negative aspects of it, and, finally, their proposals for improvement. We end this article by pointing out that the positive aspects far outnumber the negative aspects and also far exceed their initial expectations on both personal and professional levels. Furthermore, the results confirm the practical part of the seven principles of dialogic learning on which this educational action model is based.

Este trabajo se organiza en torno a la consideración de una serie de cuestiones de naturaleza teórica, metodológica y aplicada que se desprenden de un acercamiento narrativo y dialógico al estudio de la construcción de la identidad del profesorado. Se trata pues de considerar las posibles contribuciones que, una aproximación como ésta, puede realizar en relación al eje temático que da sentido a este monográfico. A saber, el estudio de la relación entre el aprendizaje y la identidad, así como el papel que las prácticas educativas formales juegan en la construcción de las identidades. El artículo está estructurado del siguiente modo: en primer lugar, se presenta, y desarrolla brevemente, una propuesta de conceptualización de la identidad docente como una construcción continua y dinámica que suponce un proceso de significación y re-significacion de las propias prácticas, vivencias y valores, influenciado por aspectos personales, sociales y culturales. Esta perspectiva supone considerar la identidad en términos de múltiples y cambiantes posiciones del yo, así como las voces que las configuran. En segundo lugar, se abordará una propuesta metodológica para el estudio de la identidad del profesorado coherente con la visión teórica de la identidad previamente presentada. En último lugar, abordaremos las tres cuestiones-claves que suponen el eje en torno al que se articula este monográfico relacionadas con las aportaciones de nuestra contribución: a la comprensión de la construcción de la identidad, a su estudio y a la elaboración de propuestas de intervención social. This work is organized around the consideration of a number of theoretical, methodological and applied issues arising from a narrative and dialogic approach to the study of teachers’ identities. We propose to consider the possible contributions that an approach like this can make in relation to the topic that gives meaning to this special issue. Namely, the study of the relationship between learning and identity, and the role that formal educational practices play in the construction of identities. The article is structured as follows: first, a proposal for the conceptualization of teacher identity as a continuous dynamic construction that involves a process of signification and re-signification of practices, experiences and values, influenced by personal, social and cultural aspects, is presented and developed briefly. This perspective implies considering identity in terms of multiples and changing I-positions as well as the voices that shape them. Second, a methodological proposal for the study of the identity of teachers consistent with the theoretical view of identity previously submitted will be addressed. Finally, we will focus on the three key issues involving the focal point around which is articulated this monograph related to the contributions of our approach: to the understanding of the construction of identity, how it can be studied and the development of proposals for social intervention

Hybrid systems are characterized by combining discrete and continuous behaviors. Verification of hybrid systems is, in general, a diffcult task due to the potential complexity of the continuous dynamics. Currently, there are different formalisms and tools which are able to analyze specific types of hybrid systems, model checking being one of the most used approaches. In this paper, we describe an extension of Java PathFinder in order to analyze hybrid systems. We apply a general methodology which has been successfully used to extend Spin. This methodology is non-intrusive, and uses external libraries, such as the Parma Polyhedra Library, to abstract the continuous behavior of the hybrid system.

The problem of verifying software systems that use dynamic data structures (such as linked lists, queues, or binary trees) has attracted increasing interest over the last decade. Dynamic structures are not easily supported by verification techniques because, among other reasons, it is difficult to efficiently manage the pointer-based internal representation. This is a key aspect when, for instance, the goal is to construct a verification tool based on model checking techniques. In addition, since new nodes can be dynamically inserted or extracted from the structure, the shape of the dynamic data (and other more specific properties) may vary at runtime, with errors such as the non desirable sharing between two nodes being difficult to detect. In this paper, we propose to use mu-calculus to describe and analyze with model checking techniques dynamic data structures such as lists and trees. The expressiveness of mu-calculus makes it possible to naturally describe these structures. In addition, following the ideas of separation logic, the logic has been extended with a new operator capable of describing the non-sharing property, which is essential when analyzing dynamic data structures.

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs.

Program synthesis with automated methods has been an active research area for many years; however, we still lack well-known and accepted techniques for this software engineering task. In this case, the design space to be considered is infinite, even when the solution is restricted to software that meets the requirements. In this paper we propose the use of model checking (MC) techniques to automatically synthesize controllers. Given a goal in the evolution of a plant, MC can be used to search for acceptable software controllers that enable the plant to evolve as desired. We also develop a realistic application in the context of a joint project with a major water reservoir management company. This application generates controllers for dam management during flood seasons. The controllers give the proper orders (open or close the outflow elements) at precise times in order to avoid disasters and to preserve the water level in the dam. Copyright © 2011 John Wiley & Sons, Ltd.

Software model checking consists in applying the most powerful results in formal verification research to programming languages such as C. One general technique to implement this approach is producing a reduced model of the software in order to employ existing and efficient tools, such as SPIN. This paper focusses on the application of this approach to the avionics software constructed on top of the Application Executive Software (APEX) Interface, which is widely employed by manufacturers in the avionics industry. It presents a method to automatically extract PROMELA models from the C source code. In order to close the extracted model during verification, we built a reusable APEX-specific environment. This APEX environment models the execution engine (i.e. an APEX compliant real-time operating system) that implements APEX services. In particular, it explains how to deal with aspects such as real-time and APEX scheduling. Time is modelled in such a way that the we save time and memory by avoiding the analysis of irrelevant steps. This model of time and the construction of a deterministic scheduler guarantees the scalability of our approach. The paper also presents a tool that can verify realistic applications, and that has been used as a novel testing method to ensure the correctness of our APEX environment. This testing method uses SPIN to execute official APEX test cases. Copyright © 2010 John Wiley & Sons, Ltd.

Most system software, including operating systems, contains dynamic data structures whose shape and contents should satisfy design requirements during execution. Model checking technology, a powerful tool for automatic verification based on state exploration, should be adapted to deal with this kind of structure. This paper presents a method to specify and verify properties of C programs with dynamic memory management. The proposal contains two main contributions. First, we present a novel method to extend explicit model checking of C programs with dynamic memory management. The approach consists of defining a canonical representation of the heap, moving most of the information from the state vector to a global structure. We provide a formal semantics of the method that allows us to prove the soundness of the representation. Secondly, we combine temporal LTL and CTL logic to define a two-dimensional logic, in time and space, which is suitable to specify complex properties of programs with dynamic data structures. We also define the model checking algorithms for this logic. The whole method has been implemented in the well known model checker SPIN, and illustrated with an example where a typical memory reader/writer driver is modelled and analyzed.

Locating potential execution errors in software is gaining more attention due to the economical and social impact of software crashes. For this reason, many software engineers are now in need of automatic debugging tools in their development environments. Fortunately, the work on formal method technologies during the past 25 years has produced a number of techniques and tools that can make the debugging task almost automatic, using standard computer equipment and with a reasonable response time. In particular, verification techniques like model-checking that were traditionally employed for formal specifications of the software can now be directly employed for real source code. Due to the maturity of model-checking technology, its application to real software is now a promising and realistic approach to increase software quality. There are already some successful examples of tools for this purpose that mainly work with self-contained programs (programs with no system-calls). However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend. In this paper, we propose a method for using the tool spin to verify C software systems that use services provided by the operating system thorough a given API. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker spin. The whole modeling process is transparent for the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we guarantee that the system only reports potential (non-spurious) errors. We present the applicability of our approach focusing on the verification of distributed software systems that use the API Socket and the network protocol stack TCP/IP for communications. In order to ensure correctness, we define and use a formal semantics of the API to conduct the construction of correct models.

A pretty wide range of concurrent programming languages have been developed over the years. Coming from different programming traditions, concurrent languages differ in many respects, though all share the common aspect to expose parallelism to programmers. In order to provide language level support to programming with more than one process, a few basic concurrency primitives are often combined to provide the main language constructs, sometimes making different assumptions. In this paper, we analyze the most common primitives and related semantics for the class of synchronous concurrent programming languages, i.e., languages with a global mechanism of processes synchronization. Then, we present a generic framework for approximating the semantics of the main constructs which applies to both, declarative as well as imperative concurrent programming languages. We determine the conditions which ensure the correctness of the approximation, so that the resulting abstract semantics safely supports program analysis and verification.

The combination of static and dynamic software analysis, such as data flow analysis (Dfa) and model checking, provides benefits for both disciplines. On the one hand, the information extracted by Dfas about program data may be utilized by model checkers to optimize the state space representation. On the other hand, the expressiveness of logic formulas allows us to consider model checkers as generic data flow analyzers. Following this second approach, we propose in this paper an algorithm to calculate Dfas using on-the-fly resolution of boolean equation systems (Bess). The overall framework includes the abstraction of the input program into an implicit labeled transition system (Lts), independent of the program specification language. Moreover, using Bess as an intermediate representation allowed us to reformulate classical Dfas encountered in the literature, which were previously encoded in terms of μ-calculus formulas with forward and backward modalities. Our work was implemented and integrated into the widespread verification platform Cadp, and experimented on real examples.

The behavior of mobile devices is highly non deterministic and barely predictable due to the interaction of the user with its applications. In consequence, analyzing the correctness of applications running on a smartphone involves dealing with the complexity of its environment. In this paper, we propose the use of model-based testing to describe the potential behaviors of users interacting with mobile applications. These behaviors are modeled by composing specially-designed state machines. These composed state machines can be exhaustively explored using a model checking tool to automatically generate all possible user interactions. Each generated trace model checker can be interpreted as a test case to drive a runtime analysis of actual applications. We have implemented a tool that follows the proposed methodology to analyze Android devices using the model checker Spin as the exhaustive generator of test cases., In Proceedings MBT 2015, arXiv:1504.01928

This paper presents the assessment of the voluntary students who have participated in centers established as Learning Community. We have carried out a content analysis of 23 reports of students of the degree in psychology from the University of Sevilla. The results have been grouped into five blocks that refer to: a) what benefit have they obtained from collaborating in the voluntary service; b) how have they felt during the collaboration; c) what are the positive aspects that they would like to highlight from the experience; d) what are the negative aspects of the experience and, lastly; e) improvement proposals that they would like to put forward. The main conclusion of this paper is that, in the view of its participants, this experience has brought them many benefits both at professional and personal levels, being a highly positively valued practice that they would recommend to others colleagues and they would repeat. En este trabajo se presentan las valoraciones de los y las estudiantes universitarios que han participado como voluntarios en centros constituidos como Comunidad de Aprendizaje. Se ha realizado un análisis del contenido de 23 informes entregados por otros tantos alumnos y alumnas de la titulación de Psicología de la Universidad de Sevilla. Los resultados se han agrupado en cinco bloques que hacen referencia a: a) para qué les ha servido colaborar en el voluntariado; b) cómo se han sentido durante esta colaboración; c) los aspectos positivos que quieren destacar de esta experiencia, d) los aspectos negativos de la misma y por último e) las propuestas de mejora que quieran formular. La principal conclusión de este trabajo es que, a juicio de los participantes, esta experiencia les ha aportado muchos beneficios a nivel profesional y personal, siendo una práctica formativa que valoran muy positivamente y que no sólo recomendarían a otros compañeros y compañeras sino que volverían a repetir.

El objetivo principal de este trabajo es identificar dimensiones relevantes del constructo Competencia Cultural Comunitaria, tanto a nivel individual —profesionales de la educación—, como a nivel organizacional —centros educativos— a través del estudio de la identidad de profesionales y centros considerados como ejemplos de buenas prácticas en la atención a comunidades diversas. Más en concreto, a través del análisis de las narrativas y actuaciones de profesionales y organizaciones, queremos identificar las ideas y creencias de profesionales y de los centros (a través del análisis de diversos materiales y de lo que sus representantes narran) sobre las actitudes y capacidades que consideran necesarias para ser competentes culturalmente ante la diversidad. Tales intereses se abordarán a través de una metodología narrativa que evidencia las estrategias y lógicas argumentativas que se elaboran a lo largo de entrevistas y debates en grupos focales. Como resultados se presentarán las competencias identificadas en los profesionales en términos de identidad profesional, a través del análisis de posiciones del yo adoptadas por los participantes (Prados, Cubero, Santamaría y Arias, 2013; Santamaría, Cubero, Prados y de la Mata, 2013); y, en las organizaciones, a través del análisis de las dimensiones de los escenarios comunitarios multiculturales ‘empoderadores’ de Maton (2008). The main objective of this work is to identify relevant dimensions of Community Cultural Competence Concept, both in an individually plane —professionals of education—, as in an organizational level —schools—. It has made through the study of identity in professionals and centres which are considered as examples of good practice in caring for diverse communities. More specifically, we analyzed the community cultural competencies through the analysis of the narratives and actions of professionals and organizations; so we identify the ideas and beliefs of professionals and centres (through the analysis of various materials and what their representatives tell us) on attitudes and capabilities deemed necessary to be culturally competent in diverse communities. Such concerns will be addressed through a narrative methodology which shows the logical and argumentative strategies that are developed along interviews and focus group discussions. The results show, in professionals, competencies in terms of professional identity, through the analysis positions taken by the participants (Prados, Cubero, Santamaría y Arias, 2013; Santamaria, Cubero, Prados y de la Mata, 2013.) and, in organizations, through the analysis of the dimensions of empowering multicultural community settings of Maton (2008).