Development of procedures for the design, optimization and manufacturing of customized orthopaedic and trauma implants: Geometrical/anatomical modelling from 3D medical imaging

Tese de Doutoramento (Programa Doutoral em Engenharia Biomédica)

A radiodifusão no Brasil e em Portugal e a invasão dos brasucas: uma nova linguagem

Tese de Doutoramento em Ciências da Comunicação (área de especialização em Sociologia da Comunicação e da Informação).

Towards the design and implementation of aspect-oriented programming for spreadsheets

A spreadsheet usually starts as a simple and singleuser software artifact, but, as frequent as in other software systems, quickly evolves into a complex system developed by many actors. Often, different users work on different aspects of the same spreadsheet: while a secretary may be only involved in adding plain data to the spreadsheet, an accountant may define new business rules, while an engineer may need to adapt the spreadsheet content so it can be used by other software systems.Unfortunately,spreadsheetsystemsdonotoffermodular mechanisms, and as a consequence, some of the previous tasks may be defined by adding intrusive “code” to the spreadsheet. In this paper we go through the design and implementation of an aspect-oriented language for spreadsheets so that users can work on different aspects of a spreadsheet in a modular way. For example, aspects can be defined in order to introduce new business rules to an existing spreadsheet, or to manipulate the spreadsheet data to be ported to another system. Aspects are defined as aspect-oriented program specifications that are dynamically woven into the underlying spreadsheet by an aspect weaver. In this aspect-oriented style of spreadsheet development, differentusers develop,orreuse,aspects withoutaddingintrusive code to the original spreadsheet. Such code is added/executed by the spreadsheet weaving mechanism proposed in this paper.

Exploring scenario exploration

Model finders are very popular for exploring scenarios, helping users validate specifications by navigating through conforming model instances. To be practical, the semantics of such scenario exploration operations should be formally defined and, ideally, controlled by the users, so that they are able to quickly reach interesting scenarios. This paper explores the landscape of scenario exploration operations, by formalizing them with a relational model finder. Several scenario exploration operations provided by existing tools are formalized, and new ones are proposed, namely to allow the user to easily explore very similar (or different) scenarios, by attaching preferences to model elements. As a proof-of-concept, such operations were implemented in the popular Alloy Analyzer, further increasing its usefulness for (user-guided) scenario exploration.

Metaphorisms in programming

This paper introduces the metaphorism pattern of relational specification and addresses how specification following this pattern can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement proposed in this paper is a strategy known as change of virtual data structure. It gives sufficient conditions for such implementations to be calculated using relation algebra and illustrates the strategy with the derivation of quicksort as example.

Development of Janus hydrogel microcapsules as novel biomaterials-stem cells construct for 3D co-culture applications

Co-cultures of two or more cell types and biodegradable biomaterials of natural origin have been successfully combined to recreate tissue microenvironments. Segregated co-cultures are preferred over conventional mixed ones in order to better control the degree of homotypic and heterotypic interactions. Hydrogel-based systems in particular, have gained much attention to mimic tissue-specific microenvironments and they can be microengineered by innovative bottom-up approaches such as microfluidics. In this study, we developed bi-compartmentalized (Janus) hydrogel microcapsules of methacrylated hyaluronic acid (MeHA)/methacrylated-chitosan (MeCht) blended with marine-origin collagen by droplet-based microfluidics co-flow. Human adipose stem cells (hASCs) and microvascular endothelial cells (hMVECs) were co-encapsulated to create platforms of study relevant for vascularized bone tissue engineering. A specially designed Janus-droplet generator chip was used to fabricate the microcapsules (<250â μm units) and Janus-gradient co-cultures of hASCs: hMVECs were generated in various ratios (90:10; 75:25; 50:50; 25:75; 10:90), through an automated microfluidic flow controller (Elveflow microfluidics system). Such monodisperse 3D co-culture systems were optimized regarding cell number and culture media specific for concomitant maintenance of both phenotypes to establish effective cell-cell (homotypic and heterotypic) and cell-materials interactions. Cellular parameters such as viability, matrix deposition, mineralization and hMVECs re-organization in tube-like structures, were enhanced by blending MeHA/MeCht with marine-origin collagen and increasing hASCs: hMVECs co-culture gradient had significant impact on it. Such Janus hybrid hydrogel microcapsules can be used as a platform to investigate biomaterials interactions with distinct combined cell populations.

Biomimetic superhydrophobic surfaces patterned with wettable spots as implantable chips for in vivo high-content 3D biomaterials response assessment

"Tissue engineering: part A", vol. 21, suppl. 1 (2015)

O género na construção de personagens 3D: do binário ao fluído

Relatório de estágio de mestrado em Média Interativos

A 3D computer assisted Orthopedic Surgery Planning approach based on planar radiography

Dissertação de mestrado integrado em Engenharia Biomédica (área de especialização em Informática Médica)

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

Fração de ejeção e volumes do ventrículo esquerdo medidos com eco 3D e com tomografia ultra-rápida

FUNDAMENTO: O ecocardiograma tridimensional em tempo real (ECO 3D) e a tomografia computadorizada ultra-rápida (CT) são dois novos métodos de análise da fração de ejeção e dos volumes do VE. OBJETIVO: Comparar as medidas da FEVE e dos volumes do VE aferidos pelo ECO 3D e pela CT ultra-rápida. MÉTODOS: Foram estudados pelo ECO 3D e pela CT ultra-rápida de 64 cortes, 39 pacientes consecutivos (27 homens, média etária de 57±12 anos). Foram analisados: FEVE e volumes do VE. Análise estatística: coeficiente de correlação (r: Pearson), teste de Bland & Altman, teste de regressão linear, 95 % IC, p<0,05. RESULTADOS: Medidas do ECO 3D: a FEVE variou de 56,1 a 78,6 (65,5±5,58)%; volume diastólico final variou de 49,6 a 178,2 (87±27,8)ml; volume sistólico final variou de 11,4 a 78 (33,1±13,6)ml. Medidas da CT: a FEVE variou de 53 a 86 (67,8±7,78)%; volume diastólico final variou de 51 a 186 (106,5±30,3) ml; volume sistólico final variou de 7 a 72 (35,5±13,4)ml. As correlações entre ECO 3D e CT foram: FEVE (r: 0,7888, p<0,0001, 95% IC 0,6301 a 0,8843); volume diastólico final (r: 0,7695, p<0,0001, 95% IC 0,5995 a 0,8730); volume sistólico final (r: 0,8119, p<0,0001, 95% IC 0,6673 a 0,8975). CONCLUSÃO: Nesta série, foi observada boa correlação entre as medidas da FEVE e entre os volumes ventriculares aferidos pelo ECO3D e pela CT ultra-rápida de 64 cortes.

"Hiper-resposta" avaliada pelo eco 3D após terapia de ressincronização cardíaca

A terapia de ressincronização cardíaca consiste em tratamento promissor para pacientes com insuficiência cardíaca grave, porém cerca de 30% dos pacientes não apresentam melhora clínica com este tratamento. Por outro lado, aproximadamente 10% dos pacientes submetidos a essa terapia podem apresentar hiper resposta, e a ecocardiografia tridimensional pode oferecer uma opção interessante para a seleção e avaliação de tratamento desses pacientes.

Comparação entre a ecocardiografia 2D e 3D na avaliação do remodelamento reverso após a TRC

FUNDAMENTO: A ecocardiografia consiste em método muito útil para seleção e avaliação de resposta à terapia de ressincronização cardíaca (TRC). O eco 3D já tem seu papel estabelecido na avaliação dos volumes ventriculares e fração de ejeção ventricular esquerda (FEVE) com excelente correlação de resultados quando comparado à RNM. OBJETIVO: Comparar a avaliação dos volumes ventriculares (VDVE, VSVE), FEVE e massa do VE antes e após a TRC pela ecocardiografia bi (Eco 2D) e tridimensional (Eco 3D). MÉTODOS: Foram avaliados 24 pacientes com IC CFIII ou IV (NYHA), ritmo sinusal QRS > 150 ms, em vigência de terapêutica otimizada para IC submetidos a TRC. Foram realizados eletrocardiograma (ECG), avaliação clínica, Eco 2D e 3D antes, três e seis meses após a TRC. A comparação entre as técnicas foi realizada utilizando-se a correlação de Pearson (r). RESULTADOS: No momento basal, a correlação entre os métodos foi de 0,96 para avaliação do VDVE, 0,95 para avaliação do VSVE, 0,87 para FEVE, e 0,72 para massa do VE. Após três meses da TRC, a correlação entre os métodos para análise do VDVE foi de 0,96, 0,95 para VSVE, 0,95 para FEVE, e 0,77 para massa do VE. Após seis meses da TRC, a correlação entre o Eco 2D e 3D para análise do VDVE foi de 0,98, 0,91 para VSVE, 0,96 para FEVE, e 0,85 para massa do VE. CONCLUSÃO: Neste estudo foi observada redução dos VDVE,VSVE, além de melhora da FEVE após a TRC. Houve excelente correlação entre o Eco 2D e o 3D para avaliação dos volumes ventriculares e FEVE, e boa correlação entre os métodos para avaliação da massa ventricular esquerda antes e após a TRC.