Safety-critical medical device development using the UPP2SF model translation tool

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in themodel-driven design of a pacemaker whosemodel is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems. © 2014 ACM.

Automatic segmentation of seven retinal layers in SDOCT images congruent with expert manual segmentation.

Segmentation of anatomical and pathological structures in ophthalmic images is crucial for the diagnosis and study of ocular diseases. However, manual segmentation is often a time-consuming and subjective process. This paper presents an automatic approach for segmenting retinal layers in Spectral Domain Optical Coherence Tomography images using graph theory and dynamic programming. Results show that this method accurately segments eight retinal layer boundaries in normal adult eyes more closely to an expert grader as compared to a second expert grader.

Neural mechanisms of context effects on face recognition: automatic binding and context shift decrements.

Although people do not normally try to remember associations between faces and physical contexts, these associations are established automatically, as indicated by the difficulty of recognizing familiar faces in different contexts ("butcher-on-the-bus" phenomenon). The present fMRI study investigated the automatic binding of faces and scenes. In the face-face (F-F) condition, faces were presented alone during both encoding and retrieval, whereas in the face/scene-face (FS-F) condition, they were presented overlaid on scenes during encoding but alone during retrieval (context change). Although participants were instructed to focus only on the faces during both encoding and retrieval, recognition performance was worse in the FS-F than in the F-F condition ("context shift decrement" [CSD]), confirming automatic face-scene binding during encoding. This binding was mediated by the hippocampus as indicated by greater subsequent memory effects (remembered > forgotten) in this region for the FS-F than the F-F condition. Scene memory was mediated by right parahippocampal cortex, which was reactivated during successful retrieval when the faces were associated with a scene during encoding (FS-F condition). Analyses using the CSD as a regressor yielded a clear hemispheric asymmetry in medial temporal lobe activity during encoding: Left hippocampal and parahippocampal activity was associated with a smaller CSD, indicating more flexible memory representations immune to context changes, whereas right hippocampal/rhinal activity was associated with a larger CSD, indicating less flexible representations sensitive to context change. Taken together, the results clarify the neural mechanisms of context effects on face recognition.

The Role of mRNA Translation in the Regulation of Ribosome Trafficking to the Endoplasmic Reticulum

The goal of this research is to identify the trafficking patterns that direct ribosomes to the endoplasmic reticulum (ER). It is widely believed that the SRP pathway is the only mechanism that cells use to localize mRNA and ribosomes to the ER, but this has been found not to be a sufficient explanation for the patterns of RNA localization in cells, namely that non-signal sequence-containing mRNA are translated on the ER and that ribosomes retain their membrane association after translation termination. First, a summary of the history of the field is presented to provide context for the key, unanswered questions in the field. Then, experiments employing [32Pi] pulse-chase labeling of HeLa cells over a time course to follow nascent ribosome trafficking are presented. The purpose of the cell labeling was to track rRNA processing and assembly into nascent ribosomes, followed by their export into the cytoplasm and recruitment into active polysomes. A detergent-based cell fractionation procedure was also utilized to separate the cytosol and ER compartments in order to observe ribosomes on their path as they exit the nucleus and either localize to the ER or cytosolic cellular compartment. Through this method, it was seen that ribosomes appear in both compartments at the same time, suggesting a mechanism may be occurring in addition to SRP-dependent ribosome trafficking. This research provides an understanding toward a mechanism that is not currently known, but will one day more fully explain the patterns of ribosomal localization.

Automatic verification of linear controller software

© 2015 IEEE.We consider the problem of verification of software implementations of linear time-invariant controllers. Commonly, different implementations use different representations of the controller's state, for example due to optimizations in a third-party code generator. To accommodate this variation, we exploit input-output controller specification captured by the controller's transfer function and show how to automatically verify correctness of C code controller implementations using a Frama-C/Why3/Z3 toolchain. Scalability of the approach is evaluated using randomly generated controller specifications of realistic size.

The DLK-1 kinase promotes mRNA stability and local translation in C. elegans synapses and axon regeneration.

Growth cone guidance and synaptic plasticity involve dynamic local changes in proteins at axons and dendrites. The Dual-Leucine zipper Kinase MAPKKK (DLK) has been previously implicated in synaptogenesis and axon outgrowth in C. elegans and other animals. Here we show that in C. elegans DLK-1 regulates not only proper synapse formation and axon morphology but also axon regeneration by influencing mRNA stability. DLK-1 kinase signals via a MAPKAP kinase, MAK-2, to stabilize the mRNA encoding CEBP-1, a bZip protein related to CCAAT/enhancer-binding proteins, via its 3'UTR. Inappropriate upregulation of cebp-1 in adult neurons disrupts synapses and axon morphology. CEBP-1 and the DLK-1 pathway are essential for axon regeneration after laser axotomy in adult neurons, and axotomy induces translation of CEBP-1 in axons. Our findings identify the DLK-1 pathway as a regulator of mRNA stability in synapse formation and maintenance and also in adult axon regeneration.