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.

Non-deterministic transducer models of retransmission protocols over noisy channels

Retransmission protocols such as HDLC and TCP are designed to ensure reliable communication over noisy channels (i.e., channels that can corrupt messages). Thakkar et al. 15] have recently presented an algorithmic verification technique for deterministic streaming string transducer (DSST) models of such protocols. The verification problem is posed as equivalence checking between the specification and protocol DSSTs. In this paper, we argue that more general models need to be obtained using non-deterministic streaming string transducers (NSSTs). However, equivalence checking is undecidable for NSSTs. We present two classes where the models belong to a sub-class of NSSTs for which it is decidable. (C) 2015 Elsevier B.V. All rights reserved.

Magnetometry using Ramsey interferometry in a Yb atomic beam

We use the Ramsey separated oscillatory fields technique in a 400 degrees C thermal beam of ytterbium (Yb) atoms to measure the Larmor precession frequency (and hence the magnetic field) with high precision. For the experiment, we use the strongly allowed S-1(0) P-1(1) transition at 399 nm, and choose the odd isotope Yb-171 with nuclear spin I = 1/2, so that the ground state has only two magnetic sublevels m(F) = +/- 1/2. With a magnetic field of 22.2 G and a separation of about 400 mm between the oscillatory fields, the central Ramsey fringe is at 16.64 kHz and has a width of 350 Hz. The technique can be readily adapted to a cold atomic beam, which is expected to give more than an order-of-magnitude improvement in precision. The signal-to-noise ratio is comparable to other techniques of magnetometry; therefore it should be useful for all kinds of precision measurements such as searching for a permanent electric dipole moment in atoms.

A novel acoustic-vibratory multimodal duet

The communication strategy of most crickets and bushcrickets typically consists of males broadcasting loud acoustic calling songs, while females perform phonotaxis, moving towards the source of the call. Males of the pseudophylline bushcricket species Onomarchus uninotatus produce an unusually low-pitched call, and we found that the immediate and most robust response of females to the male acoustic call was a bodily vibration, or tremulation, following each syllable of the call. We hypothesized that these bodily oscillations might send out a vibrational signal along the substrate on which the female stands, which males could use to localize her position. We quantified these vibrational signals using a laser vibrometer and found a clear phase relationship of alternation between the chirps of the male acoustic call and the female vibrational response. This system therefore constitutes a novel multimodal duet with a reliable temporal structure. We also found that males could localize the source of vibration but only if both the acoustic and vibratory components of the duet were played back. This unique multimodal duetting system may have evolved in response to higher levels of bat predation on searching bushcricket females than calling males, shifting part of the risk associated with partner localization onto the male. This is the first known example of bushcricket female tremulation in response to a long-range male acoustic signal and the first known example of a multimodal duet among animals.

Damage Detection Sensitivity, Specificity and Classification Data Analysis for SHM Systems Design, Verification and Validation

In this paper, we consider applying derived knowledge base regarding the sensitivity and specificity of damage(s) to be detected by an SHM system being designed and qualified. These efforts are necessary toward developing capabilities in SHM system to classify reliably various probable damages through sequence of monitoring, i.e., damage precursor identification, detection of damage and monitoring its progression. We consider the particular problem of visual and ultrasonic NDE based SHM system design requirements, where the damage detection sensitivity and specificity data definitions for a class of structural components are established. Methodologies for SHM system specification creation are discussed in details. Examples are shown to illustrate how the physics of damage detection scheme limits particular damage detection sensitivity and specificity and further how these information can be used in algorithms to combine various different NDE schemes in an SHM system to enhance efficiency and effectiveness. Statistical and data driven models to determine the sensitivity and probability of damage detection (POD) has been demonstrated for plate with varying one-sided line crack using optical and ultrasonic based inspection techniques.

Discovering compressing serial episodes from event sequences

Most pattern mining methods yield a large number of frequent patterns, and isolating a small relevant subset of patterns is a challenging problem of current interest. In this paper, we address this problem in the context of discovering frequent episodes from symbolic time-series data. Motivated by the Minimum Description Length principle, we formulate the problem of selecting relevant subset of patterns as one of searching for a subset of patterns that achieves best data compression. We present algorithms for discovering small sets of relevant non-redundant episodes that achieve good data compression. The algorithms employ a novel encoding scheme and use serial episodes with inter-event constraints as the patterns. We present extensive simulation studies with both synthetic and real data, comparing our method with the existing schemes such as GoKrimp and SQS. We also demonstrate the effectiveness of these algorithms on event sequences from a composable conveyor system; this system represents a new application area where use of frequent patterns for compressing the event sequence is likely to be important for decision support and control.

Ultrasonic Tomography and Its Applications in oilfield

UTT (Ultrasonic Tomography Tool) is widely used in the oil industry and can be used to inspect corrosion, casing wall damage, casing breakoff, and casing distortion in the well borehole with the maximum environment temperature being 125 °C, and the pressure being 60 MPa. UTT consists of tool head, upper centralization, electronic section, lower centralization, transmitters, and receivers. Its outer diameter is 4.6 cm and length is 320 cm. The measured casing diameter ranges from 60 mm to 254 mm. The tomography resolution is 512×512. The borehole measurement accuracy is 2 mm. It can supply 3D pipe tomography, including horizontal and vertical profile. This paper introduces its specification, measurement principle, and applications in oilfield.damage, casing breakoff, and casing distortion in the well borehole with the maximum environment temperature being 125 °C, and the pressure being 60 MPa. UTT consists of tool head, upper centralization, electronic section, lower centralization, transmitters, and receivers. Its outer diameter is 4.6 cm and length is 320 cm. The measured casing diameter ranges from 60 mm to 254 mm. The tomography resolution is 512×512. The borehole measurement accuracy is 2 mm. It can supply 3D pipe tomography, including horizontal and vertical profile. This paper introduces its specification, measurement principle, and applications in oilfield.

Enhanced 10-Gbit/s link performance for directly Modulated complex-coupled DFB lasers via resonance frequency, damping rate, and chirp

This paper demonstrates the respective roles that combined index- and gain-coupling play in the overall link performance of distributed feedback (DFB) lasers. Their impacts on both static and dynamic properties such as slope efficiency, resonance frequency, damping rate, and chirp are investigated. Simulation results are compared with experimental data with good agreement. Transmission-oriented optimization is then demonstrated based on a targeted specification. The design tradeoffs are revealed, and it is shown that a modest combination of index- and gain-coupling enables optimum transmission at 10 Gbit/s.

Algunas consideraciones sobre el pasado, presente y futuro de Europa

Resumen: El objetivo del presente trabajo es hacer un recorrido sobre los diversos lugares desde donde el pensamiento antiguo clásico ha abordado a “Europa” como concepto y como realidad. En primer lugar, indagando en sus testimonios se analizará cómo éstos fueron construyendo y transformando una conciencia geográfica del espacio territorial europeo. En segundo lugar, se esbozará la forma en que fue estructurándose, en principio, el “mito” de Europa como diosa, para luego ver cómo se estructuró la “idea” de Europa, afirmándose fundamentalmente en oposición al Asia y consolidándose en la asociación de continente y Cristiandad en tiempos medievales. Por último, se analizará el concepto como realidad histórica, para finalmente reflexionar brevemente sobre la situación de la cultura y cosmovisión europea en el siglo XX hasta hoy.

Relatos de viajes medievales : una historia de taxonomías literarias (1849-2007)

Número monográfico: El viaje y sus discursos

Mesofracture mechanics: a necessary link

Classical fracture mechanics is based on the premise that small scale features could be averaged to give a larger scale property such that the assumption of material homogeneity would hold. Involvement of the material microstructure, however, necessitates different characteristic lengths for describing different geometric features. Macroscopic parameters could not be freely exchanged with those at the microscopic scale level. Such a practice could cause misinterpretation of test data. Ambiguities arising from the lack of a more precise range of limitations for the definitions of physical parameters are discussed in connection with material length scales. Physical events overlooked between the macroscopic and microscopic scale could be the link that is needed to bridge the gap. The classical models for the creation of free surface for a liquid and solid are oversimplified. They consider only the translational motion of individual atoms. Movements of groups or clusters of molecules deserve attention. Multiscale cracking behavior also requires the distinction of material damage involving at least two different scales in a single simulation. In this connection, special attention should be given to the use of asymptotic solution in contrast to the full field solution when applying fracture criteria. The former may leave out detail features that would have otherwise been included by the latter. Illustrations are provided for predicting the crack initiation sites of piezoceramics. No definite conclusions can be drawn from the atomistic simulation models such as those used in molecular dynamics until the non-equilibrium boundary conditions can be better understood. The specification of strain rates and temperatures should be synchronized as the specimen size is reduced to microns. Many of the results obtained at the atomic scale should be first identified with those at the mesoscale before they are assumed to be connected with macroscopic observations. Hopefully, "mesofracture mechanics" could serve as the link to bring macrofracture mechanics closer to microfracture mechanics.

El redescubrimiento de la filosofía personalista de Jacques Maritain

Resumen: El autor sostiene que la búsqueda de nuevos modelos empresariales y de política económica nos invita a redescubrir la filosofía personalista de Maritain. En el núcleo de la obra Humanismo integral (1936) del filósofo francés aparece la idea de que el hombre es una persona "de naturaleza espiritual, dotada de libre albedrío, y por lo tanto autónoma en relación con el mundo". El artículo estudia la naturaleza del bien común temporal, que para Maritain se relaciona con la vida buena de la toda la comunidad –el bien común o bonum commune– tanto en el sentido material como moral. Este bonum commune no es el objetivo final del orden temporal, sino que está subordinado a lo que trasciende el bienestar temporal de la persona humana –la realización de la libertad y la perfección espiritual. En última instancia, el orden nunca se completa. El balance definitivo o telos nunca se obtiene ya que el hombre está siempre en camino.

Umbrales del relato y autorreferencia en los libros de viajes españoles contemporáneos

Número monográfico: El viaje y sus discursos

Problemas en torno a la filosofía de la educación

Resumen: Se analizan en este artículo la complejidad que tiene una filosofía de la educación, sea desde el punto de vista de lo que es ya un sistema filosófico; sea ya por la complejidad del ser humano y la sociedad humana. En segundo lugar se analiza la complejidad contenida en el concepto de educación y las dificultades de su formulación en una definición y en una teoría filosófica educativa. El autor, por su parte, propone a consideración una posible definición de educación, integral e integradora, buscando recomponer una visión parcializada y centrada en el desarrollo casi exclusivamente intelectual.

Fray Servando de Mier y su sermón guadalupano de 1794 : la búsqueda de una justificación teológica a la independencia de América

Resumen: Fray Servando Teresa de Mier, de la orden de Santo Domingo, fue uno de los tantos religiosos criollos comprometidos con la independencia. En este trabajo se toma el famoso sermón que predicara en la Colegiata de Guadalupe en el año 1794, en el cual buscó explicar y justificar una mítica proto-evangelización de México, anterior a la llegada de los españoles, con el fin velado de quitarle a España uno de los títulos de dominio sobre América, el de Evangelizadora, en busca de una justificación teológica a la Emancipación.