Formal Aspects in SDH for Children in Spanish Television: A Descriptive Study

The comprehension of a subtitle goes far beyond the understanding of the meaning of the words it comprises. Formal aspects of subtitles for the d/Deaf and the hard-of-hearing (SDH) can be crucial in the cognitive effort necessary to process the subtitle within its audiovisual context (Perego 2008). The present article studies common practices of formal aspects in SDH for children, focusing on three parameters: layout and positioning of the subtitle; orthotypographic conventions; and resources for the identification of characters in the three TV channels dedicated exclusively to the youngest audiences in Spain. The present piece of research was carried out by analysing and evaluating these three parameters in comparison with the current UNE Standard 153010 (AENOR 2012) and with previous theoretical studies in the field.

Using formal reasoning on a model of tasks for FreeRTOS

FreeRTOS is an open-source real-time microkernel that has a wide community of users. We present the formal specification of the behaviour of the task part of FreeRTOS that deals with the creation, management, and scheduling of tasks using priority-based preemption. Our model is written in the Z notation, and we verify its consistency using the Z/Eves theorem prover. This includes a precise statement of the preconditions for all API commands. This task model forms the basis for three dimensions of further work: (a) the modelling of the rest of the behaviour of queues, time, mutex, and interrupts in FreeRTOS; (b) refinement of the models to code to produce a verified implementation; and (c) extension of the behaviour of FreeRTOS to multi-core architectures. We propose all three dimensions as benchmark challenge problems for Hoare's Verified Software Initiative.

Soundness of workflow nets: classification, decidability, and analysis

Workflow nets, a particular class of Petri nets, have become one of the standard ways to model and analyze workflows. Typically, they are used as an abstraction of the workflow that is used to check the so-called soundness property. This property guarantees the absence of livelocks, deadlocks, and other anomalies that can be detected without domain knowledge. Several authors have proposed alternative notions of soundness and have suggested to use more expressive languages, e.g., models with cancellations or priorities. This paper provides an overview of the different notions of soundness and investigates these in the presence of different extensions of workflow nets.We will show that the eight soundness notions described in the literature are decidable for workflow nets. However, most extensions will make all of these notions undecidable. These new results show the theoretical limits of workflow verification. Moreover, we discuss some of the analysis approaches described in the literature.

Untanglings: A novel approach to analyzing concurrent systems

Substantial research efforts have been expended to deal with the complexity of concurrent systems that is inherent to their analysis, e.g., works that tackle the well-known state space explosion problem. Approaches differ in the classes of properties that they are able to suitably check and this is largely a result of the way they balance the trade-off between analysis time and space employed to describe a concurrent system. One interesting class of properties is concerned with behavioral characteristics. These properties are conveniently expressed in terms of computations, or runs, in concurrent systems. This article introduces the theory of untanglings that exploits a particular representation of a collection of runs in a concurrent system. It is shown that a representative untangling of a bounded concurrent system can be constructed that captures all and only the behavior of the system. Representative untanglings strike a unique balance between time and space, yet provide a single model for the convenient extraction of various behavioral properties. Performance measurements in terms of construction time and size of representative untanglings with respect to the original specifications of concurrent systems, conducted on a collection of models from practice, confirm the scalability of the approach. Finally, this article demonstrates practical benefits of using representative untanglings when checking various behavioral properties of concurrent systems.

On the expressive power of behavioral profiles

Behavioral profiles have been proposed as a behavioral abstraction of dynamic systems, specifically in the context of business process modeling. A behavioral profile can be seen as a complete graph over a set of task labels, where each edge is annotated with one relation from a given set of binary behavioral relations. Since their introduction, behavioral profiles were argued to provide a convenient way for comparing pairs of process models with respect to their behavior or computing behavioral similarity between process models. Still, as of today, there is little understanding of the expressive power of behavioral profiles. Via counter-examples, several authors have shown that behavioral profiles over various sets of behavioral relations cannot distinguish certain systems up to trace equivalence, even for restricted classes of systems represented as safe workflow nets. This paper studies the expressive power of behavioral profiles from two angles. Firstly, the paper investigates the expressive power of behavioral profiles and systems captured as acyclic workflow nets. It is shown that for unlabeled acyclic workflow net systems, behavioral profiles over a simple set of behavioral relations are expressive up to configuration equivalence. When systems are labeled, this result does not hold for any of several previously proposed sets of behavioral relations. Secondly, the paper compares the expressive power of behavioral profiles and regular languages. It is shown that for any set of behavioral relations, behavioral profiles are strictly less expressive than regular languages, entailing that behavioral profiles cannot be used to decide trace equivalence of finite automata and thus Petri nets.

Avaliação de textos produzidos na aula de língua portuguesa: abordagens teóricas, questões didático-metodológicas e suas repercussões

Dentro do contexto da avaliação formativa, as práticas de correção dos textos produzidos devem ser entendidas não como medição da aprendizagem, mas principalmente como uma pesquisa, elas devem avaliar o aluno, o professor, o processo, as práticas enunciativas, a mediação, a escola e mesmo a família. Contudo, apesar de essa abordagem sobre a avaliação ser compatível com a concepção sócio-histórica e cognitiva da linguagem, que por sua vez é consoante com as orientações dos PCN de Língua Portuguesa, ela parece ainda se mostrar distante dos métodos adotados pelos professores. O objetivo geral desta dissertação é identificar as abordagens teóricas que subjazem aos métodos avaliativos de professores do ensino fundamental em relação à produção textual. Como objetivos específicos buscou-se (i) mapear os modelos de correção textual utilizado por esses professores a fim de oferecer um panorama sobre a realidade do ensino-aprendizagem da escrita; e (ii) organizar um material teórico capaz de embasar a prática avaliativa não apenas como um componente do ato pedagógico, mas também como componente simbólico da construção da imagem que o aluno tem sobre si e sobre sua capacidade de escrever. Trata-se de uma pesquisa qualitativa constituída por dois corpora, organizados a partir dos seguintes instrumentos: entrevista semiestruturada com sete professores que lecionam no terceiro e quarto ciclos do ensino fundamental em escolas públicas e/ou particulares; e textos escritos por alunos e corrigidos pelos mesmos professores-informantes. Constituindo um total de 35 documentos, cinco de cada professor e 3h48min de gravações transcritas. Para análise dos corpora optou-se pelo paradigma interpretativista, aliado ao paradigma indiciário, que busca olhar para além das recorrências, os dados episódicos, singulares, dados que possam ajudar a levantar hipóteses sobre uma realidade não observável por via direta. Em relação às abordagens teóricas, podem-se perceber três manifestações: (i) as que são focadas no sistema, observável quando o professor privilegia aspectos formais e quando suas marcações, ainda que busquem o aspecto discursivo, não são suficientes para que os alunos efetuem reflexões sobre o uso da língua; (ii) as que flutuam entre o estruturalismo e o sociointeracionismo, quando o professor, embora se utilize de práticas mais interacionais ainda deixa amplo espaço para correções formais; (iii) as que são eminentemente sociointeracionistas, em cujas marcas avaliativas pode-se observar respeito pela autoria, apreciação do texto, interferência significativa e convite à reflexão. Dessas práticas emergem dois papéis sociais dicotômicos assumidos pelo professor: o de revisor, que tem profunda relação com práticas avaliativas de medição, e o de leitor-avaliador, em que se pode perceber, além de métodos ligados ao sociointeracionismo e às práticas avaliativas formativas um outro aspecto singular: a afetividade. Para discorrer sobre cada um desses aspectos propostos, construiu-se uma revisão bibliográfica que buscou incorporar à discussão teórico-metodológica questões de ordem subjetivas, que orientam pensar a escrita não só sob seu aspecto sócio-histórico e cognitivo, mas também afetivo

Quando a palavra está ligada ao corpo e o corpo à palavra (um ensaio dramático)

O objetivo desta tese é, por um lado, abordar a relação entre o corpo e a linguagem a partir das perspectivas da poesia, do teatro e da performance. Por outro lado, propomos que a compreensão de tal campo relacional pode esclarecer pontos em comum entre essas diferentes artes, trazendo uma nova percepção do fenômeno poético. Para tal, fez-se necessário operar um desvio com relação à concepção moderna que entende o corpo enquanto substância material extensa e a linguagem como algo associado à substância subjetiva ideal do pensamento. Pelo contrário, procuramos trabalhar com a hipótese de que corpo e linguagem se encontram em estado de relação senão necessária ao menos constante, valendo-nos da ideia do corpo-em-vida, e da linguagem enquanto ação e enquanto discurso. A análise opera um recorte contemporâneo entre obras que vão das poetas Angélica Freitas e Marília Garcia até a da atriz e encenadora Cristina Flores, e da performer norte-americana Laurie Anderson. A escrita da tese nos levou a uma combinação entre aspectos formais do ensaio e do drama, numa costura de múltiplas vozes, de modo a concretizar o entrelaçamento entre as ideias vividas ao longo da pesquisa e a experiência física da produção do texto

LUCIANO BERIO’S NATURALE: A STORY COMBINING FOLK MUSIC AND ART MUSIC

The study of a score by a serious performer is a fundamental step in the process of arriving at a knowledgeable and deeply informed approach to performing a piece of music. In order to obtain this knowledge numerous aspects of the score must be taken into consideration. It is the intent of this dissertation to gather and analyze the information concerning Naturale, a work written by Luciano Berio in 1985 for viola, percussion and recorded voice, based on Sicilian folk songs. All the aspects surrounding Naturale’s existence are taken into consideration in this study. First, it is important to reflect on Berio’s compositional style and traits, the manner in which he relates his works one to another, what he sees in folk music and his own personal desire to intertwine art music and folk music. For Berio Naturale is not an isolated venture into the realm of mixing folk music and his own avant-garde style; it is instead one of many works resulting from his long-standing relationship with folk music. Another essential aspect in this case is the study of Sicilian folk music itself, and the sources used by Berio to find the songs by which he was inspired. The work is examined section by section with figures showing both excerpts of Naturale as well as the original songs with their translations. An analysis containing harmonic, thematic and formal aspects of the score was developed in order to arrive at a better understanding of the structure and pacing of the piece. For this research the author went to Italy to conduct an interview with Maestro Aldo Bennici, the Sicilian violist for whom Naturale was composed. This interview helped in the discovery of two more songs used by Berio that have not to this point been identified in any other document. Bennici’s outstanding testimony portrayed the expressive character of this music and the evocative imagery behind this score. I hope to bring this knowledge to other performers, that they may fully understand and appreciate the unique beauty and power of Berio’s Naturale.

Astonishing apples: visualising the novel

This paper explores the developing relationship between fictional and visual representations. The impact of visual art on the novel as mimetic is an issue that writers have engaged with and written about from the mid-nineteenth century to the present day, often raising the question of the art/life dialectic and how it has evolved through the novel’s exploration of ideas. From painting, photography, cinema, television and newer digital visual cultures writers have sought to involve themselves in a critical examination of the impact of changes in these forms on other art form and on wider society. How do these visual forms affect what it means to be an artist, a writer, a human being? The paper takes the work of Paul Cezanne as a starting point in the history of representation. Writers such as Rainer Maria Rilke, theorists such as Maurice Merleau-Ponty, and other artists like Picasso, have been influenced by, or responded to, Cezanne’s work and to Cezanne’s writings on art and his letters to his great childhood friend, the novelist Emile Zola. By discussing the creative practice of writing a novel this paper will examine questions of how the novel can, and should, respond to the impact of visual culture’s seeming dominance over other art forms. It also explores what impact new forms of visual culture have had upon the mimetic and formal aspects of the novel and how the novel works as representational, especially in relation to representations of human consciousness. [From the Author]

El análisis de libros de texto: una estrategia metodológica en la formación de los profesionales de la educación

A pesar de la progresiva introducción de nuevos recursos en las aulas fruto del desarrollo de las TICs, el libro de texto sigue siendo uno de los materiales más utilizado y cuyo protagonismo en la configuración de la práctica escolar ha sido decisivo, por lo que debe ocupar nuestra atención en la formación inicial de los profesionales de la educación. Durante los cursos académicos 2012-13 y 13-14, hemos realizado en el marco de la asignatura de Análisis y diseño de materiales para la educación y la formación del tercer curso del grado de Pedagogía de la Universidad de Oviedo una práctica formativa de análisis de libros de texto escolares que nos ha permitido analizar contextualizadamente y desde una perspectiva teórico-práctica, cuestiones tales como: papel del profesorado en el desarrollo e innovación del currículum, papel de las editoriales en la interpretación del currículum oficial, análisis de tareas y mensajes en los manuales escolares, criterios para juzgar la calidad didáctica de los materiales, etc. El análisis cualitativo de treinta informes desarrollados por 120 estudiantes sobre diferentes libros de texto nos ha permitido identificar sus principales fortalezas y debilidades en varias dimensiones (aspectos formales, metodología, mensajes, implicaciones para la profesionalidad docente) y nos permite concluir que se trata de una experiencia formativa relevante en la formación inicial de cualquier profesional de la educación.