Singularidades de gênero no cuidado psicossocial às usuárias de cocaína e crack: contribuições para a enfermagem

O consumo de cocaína e crack gera importantes repercussões para saúde. Em relação aos usuários destas drogas, há predomínio dos homens sobre as mulheres. Em virtude das mulheres serem o grupo minoritário, o cuidado de saúde mental nem sempre observa as especificidades do gênero feminino e suas vulnerabilidades no processo saúde-doença. Para investigar esta problemática, foi proposto o objeto de estudo "As singularidades do gênero feminino no cuidado psicossocial às usuárias de cocaína e crack". Delimitaram-se os seguintes objetivos: Analisar o cuidado psicossocial às mulheres usuárias de Crack e Cocaína e Discutir a abordagem das singularidades do gênero feminino neste cuidado. Adotou-se como referencial teórico da pesquisa a categoria Gênero. Para alcançar estes objetivos, optou-se por pesquisa qualitativa, que foi desenvolvida no único CAPS ad do município de Duque de Caxias, localizado na Baixada Fluminense do Estado do Rio de Janeiro. Os participantes da pesquisa foram profissionais de saúde que exercem o cuidado das mulheres usuárias de cocaína e crack. Para coleta de dados, utilizou-se a triangulação de técnicas: a) observação sistemática nos espaços de cuidado coletivo; b) entrevistas semiestruturadas com os profissionais de saúde e c) análise documental dos prontuários das mulheres. A análise dos dados empíricos foi orientada pela Hermenêutica-Dialética. Foram analisados 113 prontuários das mulheres assistidas no CAPS ad. A maioria das mulheres estava na faixa etária de 20 a 34 anos, solteiras, mães com prole menor de idade, que viviam com os familiares, não tinham fonte de renda própria e envolvimento com a justiça. Quase a totalidade utilizava também outras drogas, como tabaco, maconha e álcool. Foram entrevistados 17 profissionais de saúde. As categorias da pesquisa foram: Concepções dos profissionais sobre o cuidado psicossocial: centrado na pessoa e centrado na doença; as questões do gênero feminino e as usuárias de crack e cocaína; a condição feminina e suas influências no cuidado psicossocial. As singularidades de gênero no cuidado psicossocial foram reveladas no comportamento e enfrentamento das mulheres frente ao uso de cocaína e crack, mas também nas estratégias de cuidado adotadas pelos profissionais. O cuidado psicossocial por vezes reforça os estereótipos de gênero e, por outra, estimula o exercício da autonomia feminina. Os profissionais apresentaram percepções determinadas pelas questões de gênero, atribuindo às mulheres características distintivas, como a "fragilidade" e a dependência emocional, que interferem nas vivências femininas acerca do uso de cocaína e crack. A prostituição surgiu como uma consequência da vulnerabilidade do gênero feminino no contexto de consumo de drogas. Recomenda-se a implementação de ações programáticas direcionadas para as singularidades da clientela feminina e a discussão das iniquidades de gênero no âmbito da formação profissional, da assistência e da pesquisa para superar a práxis reducionista e a naturalização das diferenças e da subalternidade feminina nestes espaços de produção de saúde. Como integrante da equipe de saúde, enfermeiros e auxiliares de enfermagem necessitam estar sensibilizados para as questões de gênero e terem uma maior participação no cuidado individual e coletivo desta clientela.

Estudo transversal sobre a exposição às tecnologias não-invasivas de cuidado de enfermagem obstétrica na atenção ao parto e sua repercussão na vitalidade do recém-nascido

Estudo cujo objeto foi o emprego de tecnologias não-invasivas de cuidado de enfermagem obstétrica (TNICEO) por enfermeiras obstétricas durante o acompanhamento do trabalho de parto e parto, e suas repercussões sobre a vitalidade do recém-nascido. A tese é: a disponibilização de TNICEO pelas enfermeiras obstétricas na atenção ao trabalho de parto, parto e nascimento está associada a recém-natos com índice de Apgar (IA) >8, quando comparado com o índice de Apgar de recém-nascidos cujas mães não puderam optar pelo uso destas tecnologias. Objetivou: a) descrever as características obstétricas das mulheres e de seu trabalho de parto e parto acompanhados por enfermeiras obstétricas; b) descrever as TNICEO disponibilizadas pelas enfermeiras obstétricas no cuidado à parturiente; c) medir e comparar a associação entre o IA de primeiro e quinto minutos de vida dos recém-nascidos cujas mães fizeram uso das TNICEO com: o IA do primeiro e quinto minutos de vida dos recém-nascidos cujas mães foram submetidas ao tratamento tradicional (intervenções); o IA do primeiro e quinto minutos de vida dos recém-nascidos cujas mães utilizaram tanto TNICEO e assistência tradicional (AT); o IA do primeiro e quinto minutos de vida dos recém-nascidos cujas mães e não foram submetidas a nenhum tipo de assistência (TNICEO ou AT) durante o trabalho de parto. Tratou-se de estudo observacional descritivo, transversal, retrospectivo. Realizado em Hospital Maternidade Municipal localizado na zona norte do Município do Rio de Janeiro. A amostra foi 6.790 parturientes, que tiveram parto vaginal acompanhado por enfermeiras obstétricas, entre setembro/2004 e dezembro/2011. A fonte de informações foi o Livro de Registros de Partos (LRP) da maternidade. Os resultados evidenciaram que: 91,9% utilizaram um ou mais recurso relacionado às TNICEO e 60,2% foram submetidas a uma ou mais intervenção da AT. Quanto ao IA no 1 e no 5 minuto de vida, com relação às variáveis relacionadas aos tipos de assistência que utilizaram, constatou-se que os neonatos cujas mães durante o trabalho de parto e parto utilizaram algum tipo de TNICEO apresentaram percentuais mais elevados de IA > 8, tanto no 1 minuto (93,4%) como no 5 minuto de vida (99,0%). Em contrapartida os neonatos cujas mães foram submetidas a algum procedimento relacionado à AT apresentaram os menores percentuais de IA (82,8%) no 1 minuto e (94,7%) no 5 minuto de vida. Confirmando a tese proposta, conclui-se que a razão de chance do IA ser > 8 no primeiro minuto de vida é aumentada (OR 4,564; IC95%: 1,887 11,038; p valor 0,0008) a favor do grupo de mulheres que utilizaram apenas as TNICEO durante TP e/ou P, comparado ao grupo de mulheres submetidas às intervenções da AT. Referente ao quinto minuto de vida, a razão de chance de um recém-nascido cuja mãe que teve seu TP e/ou P acompanhados pelas enfermeiras obstétricas e utilizaram as somente as TNICEO na assistência foi maior (OR = 4,927; IC95% 2,349 10,334 ; p valor 0,00020), quando comparado com o grupo de parturientes da AT.

Cuidado em saúde à pessoa que vive com HIV/Aids: representações sociais de enfermeiros e médicos

O presente estudo tem como objetivos identificar as representações sociais do cuidado em saúde à pessoa que vive com HIV/aids para enfermeiros e médicos, descrevendo-as através das abordagens estrutural e processual; comparar as representações de enfermeiros e médicos; e analisar o cuidado em saúde à pessoa que vive com HIV/aids a partir das representações construídas por esses profissionais. Trata-se de um estudo descritivo com abordagem qualitativa, orientado pela Teoria das Representações Sociais. Os participantes do estudo foram, numa primeira etapa, 81 profissionais, sendo 54 médicos e 27 enfermeiros que trabalham em instituições públicas com atuação voltada à testagem e ao atendimento à pessoa que vive com HIV/aids, onde responderam ao questionário sócio-profissional e de evocações livres. Na segunda etapa, conforme conveniência, participaram da entrevista semi-estruturada, 20 enfermeiros e 18 médicos. Para a análise dos dados utilizamos a técnica do quadro de quatro casas com a utilização do software EVOC 2005 e a análise lexical pelo software Alceste 4.0. Quanto à estrutura representacional geral, destaca-se no Núcleo Central os termos acolhimento, adesão-tratamento, futuro e informação, que refletem a estruturação do processo assistencial da prática do cuidado no seio do programa. Na zona de contraste foram identificados atenção, cuidado e educação-saúde, que reforçam o Núcleo Central. Destaca-se, ainda, o léxico cuidado trazendo a dimensão imagética da representação. Na análise realizada pelo Alceste foram definidas cinco classes: estrutura e dinâmica de atendimento às pessoas que vivem com HIV/aids; o processo de transmissão e de prevenção do HIV/aids: entre vítimas, culpados e profissionais; memórias e história da epidemia de HIV/aids contada por profissionais; o cuidado no contexto da equipe multidisciplinar: composição, desafios e conceitos; o programa nacional DST/Aids e sua implementação nas unidades de saúde: avaliação, memória e capacitação. Realizamos ainda, a análise cruzada dos termos cuidado de enfermagem e cuidado médico. Ao final do estudo, consideramos que a representação do cuidado em saúde para este grupo de profissionais mostrou-se positiva apesar das dificuldades encontradas em seu cotidiano laboral. A representação do cuidado em saúde à pessoa vivendo com HIV/aids para médicos e enfermeiros apoia-se no programa DST/Aids e no conhecimento científico que embasa cada profissão. Os profissionais valorizam o trabalho multidisciplinar e procuram tratar o cliente de forma respeitosa, incentivando a adesão ao tratamento através de informação e do apoio psicológico.

O cuidado prestado pela família à criança portadora de encefalopatia hipóxico-isquêmica no contexto domiciliar: contribuições para a enfermagem

Os avanços tecnológicos ocorridos nas últimas três décadas na área da saúde têm garantido a sobrevivência de crianças nascidas extremamente prematuras ou asfíxicas, o que acabou gerando as chamadas crianças com necessidades especiais de saúde, dentre elas, as portadoras de encefalopatia hipóxico-isquêmica. A encefalopatia acomete as crianças em graus variados requerendo cuidados específicos, o que implica na inclusão de suas famílias nas ações de cuidados a criança quando no domicílio. Objeto de estudo: o cuidado prestado pela família à criança portadora de encefalopatia hipóxico-isquêmica no contexto domiciliar. Objetivos: descrever as demandas de cuidados da criança portadora de encefalopatia no domicílio, identificar as práticas de cuidados desenvolvidas pelos familiares cuidadores junto a essas crianças e discutir os desafios determinados por esses cuidados para os familiares cuidadores de criança com encefalopatia no domicílio. Metodologia: pesquisa qualitativa, desenvolvida a partir do método criativo sensível, utilizando a dinâmica corpo-saber no domicílio de cinco grupos de familiares cuidadores, totalizando doze familiares. O período de geração dos dados ocorreu de fevereiro a abril de 2014. Os dados foram analisados a partir da análise de discurso, em sua corrente francesa, e interpretados à luz da concepção freiriana, com destaque para os conceitos de crítica reflexiva, processo de conscientização e educação dialógica e o cuidado centrado na família. Resultados: as práticas de cuidados dos familiares apontaram modificações nos cuidados habituais de alimentação, higiene, desenvolvimento e medicamentoso. Na prática da alimentação, os familiares expressaram suas condutas frente à alimentação por via oral ou por gastrostomia e suas crenças e atitudes frente a essas práticas alimentares. Quanto à higiene, revelaram a necessidade de adaptações na prática habitual do banho. No que se refere aos cuidados voltados ao desenvolvimento, apontaram o lazer e as brincadeiras como elementos adjuvantes ao favorecimento do desenvolvimento infantil. O cuidado medicamentoso emergiu como parte do universo das famílias, apontando a necessidade dos profissionais de saúde, em especial, os da enfermagem, incluírem esta temática em suas pautas de orientações. Quanto aos desafios vividos pelos familiares, esses estiveram relacionados ao medo e a inexperiência no cuidar da criança, ao enfrentamento e a aceitação da necessidade especial de saúde, a necessidade de uma rede de solidariedade cooperando nas dificuldades econômicas e ao atendimento em saúde por diferentes profissionais e especialidades. Conclusão: as múltiplas dimensões de cuidados apresentadas pelas crianças com necessidades especiais de saúde apontam para o profissional de enfermagem a necessidade de desenvolver seu papel educador junto aos familiares pautado na dialogicidade e horizontalidade facilitando, assim, a relação com os estes, em benefício da criança e promovendo a aproximação profissional/família, O estudo assinala a necessidade de dos profissionais de saúde, em especial, o enfermeiro, perceberem a família como um elemento chave no processo de cuidar da criança com necessidades especiais de saúde quando no domicílio.

Dinâmica socioeconômica do município de Macaé/RJ: uma análise do mercado de trabalho formal após a quebra do monopólio na exploração do petróleo

Esta tese tem por objetivo analisar as transformações socioeconômicas, com ênfase na dinâmica do mercado de trabalho, que ocorreram no município de Macaé, principalmente após a promulgação da Lei n 9.478, de 06/08/1997. Esta lei acabou com o monopólio da petrobras no que concerne a prospecção de petróleo atraindo para a região inúmeras empresas multinacionais. A importância do estudo deste municípío se deve ao fato de Macaé exercer um importante papel economico na retomada do crescimento da economia do Estado do Rio de Janeiro em funçaõ da indústria petrolífera e seus impactos estarem além de suas fronteiras, repercurtindo em toda a região norte fluminense e municípios da baixada litorãnea. Outro aspecto abordado é a forma como a região norte fluminense sempre esteve ligada aos projetos de desenvolvimento de nosso país, principalmente no que diz respeito a políticas energéticas, como o proálcool e o petróleo. Macaé tornou-se um pólo econômico muito forte para o capital porém, as contradições do sistema capítalista caminham na mesma proporção que o dinheiro do petróleo, logo as desigualdades sociais despontam de maneira muito forte e o mercado de trabalho local reflete esta contradição.

Memória social de enfermeiros acerca do cuidado de Enfermagem no contexto do HIV/aids: enfrentamentos, afetos e construções representacionais

Este estudo tem como objeto o cuidado de Enfermagem e suas memórias e representações sociais para enfermeiros hospitalares inseridos nas unidades de referências para pessoas que viviam com o HIV/aids no Rio de Janeiro, no decorrer de 1980 a 1991. Os objetivos específicos foram: identificar a memória social do cuidado de enfermagem implementado pelos enfermeiros aos acometidos pelo HIV/aids no Município do Rio de Janeiro; descrever as práticas de cuidado pelos enfermeiros no contexto do recorte temporal adotado no estudo; descrever o processo de enfrentamento da epidemia da aids pelos enfermeiros, tanto no contexto do cuidado de enfermagem no espaço hospitalar, quanto nas relações sociais estabelecidas; analisar as memórias e representações sociais de enfermeiros acerca do cuidado de Enfermagem prestado às pessoas com HIV/aids em situação de hospitalização na primeira década da epidemia. Trata-se de uma pesquisa descritiva, de campo, com abordagem qualitativa, baseada nos pressupostos teóricos da memória social propostos por Sá em sua interface com a teoria de representações sociais no campo da Psicologia Social. Realizada com 30 enfermeiros que atuaram em hospitais considerados de referência para o tratamento de clientes que viviam com HIV/aids. Os dados foram coletados por uma entrevista semiestruturada e a visualização de 12 fac-símiles escolhidos de forma aleatória na imprensa. A população de estudo é predominantemente do sexo feminino e com idade entre 51 a 60 anos. Os principais resultados apontam que a memória social do cuidado de enfermagem se constitui a partir de diferentes objetos representacionais (cuidado de enfermagem, aids e biossegurança), instâncias da memória social (pessoal, pública, prática, coletiva, comuns, histórica oral e histórica documental) e diversos elementos que constituem esta memória (ambiente de cuidado e relações sociais, familiares e laborais, dentre outras). Emergiram sete categorias de análise: O processo do cuidado de Enfermagem: do enfrentamento, da capacitação e do desenvolvimento; Sentimentos dos enfermeiros e dos clientes descritos pelos participantes no processo de cuidar; O processo de cuidado direto ao cliente no início da epidemia; Memórias da autoproteção profissional e da proteção ao cliente no contexto do HIV/aids; Os contextos do cuidado: ambiente, materiais e recursos humanos; Memórias dos enfermeiros sobre os clientes acometidos pelo HIV e Relacionamento interpessoal. Destaca-se que a memória do cuidado de enfermagem se mostra ligada à construção representacional da aids (não familiar/familiar), do cuidado de enfermagem (sem controle/sob controle) e à constituição de um grupo social com forte identidade, o dos enfermeiros da aids. Concluímos que o estudo mostrou o trabalho pioneiro dos enfermeiros com o HIV/aids no ambiente hospitalar. Esses profissionais tiveram que cuidar desses clientes em meio à possibilidade de contaminação, ao mesmo tempo em que desenvolviam um autocuidado, em alguns momentos exagerados devido ao desconhecimento sobre a síndrome, como forma de preservação da sua saúde, bem como de sua família. A memória social como conceito guarda-chuva mostrou-se pertinente para a análise dos dados, permitindo recuperar, ao menos em parte, a dinâmica do cuidado de enfermagem nos primeiros anos da síndrome.

O acolhimento de usuários no centro cirúrgico e a humanização das práticas cotidianas do cuidado de enfermagem

Falar da humanização é retomar a tradição do ocidente de pensar o lugar que o ser humano ocupa no mundo, nas inter-relações com seus semelhantes, na esfera social e também de saúde, em uma ética e solidariedade. Para uma prática de cuidados humanizada, o início destes cuidados deve ocorrer com o acolhimento do usuário em todos os setores, entre eles o Centro Cirúrgico. Este estudo tem como objetivo geral: compreender o processo de acolhimento no cotidiano da assistência de enfermagem no Centro Cirúrgico a partir da diretriz: acolhimento, ambiência e clínica ampliada da Política Nacional de Humanização. E como objetivos específicos: descrever o acolhimento do usuário durante as práticas cotidianas do cuidado de enfermagem no Centro Cirúrgico; analisar as experiências de acolhimento na perspectiva dos usuários no Centro Cirúrgico durante as práticas cotidianas do cuidado de enfermagem e identificar as estratégias utilizadas durante o cuidado de enfermagem no Centro Cirúrgico que concretizam a viabilização da diretriz: acolhimento, ambiência e clínica ampliada. Para dar conta do estudo selecionamos a abordagem etnometodológica, caráter exploratório. O cenário do estudo foi um hospital da rede estadual do Rio de Janeiro e os dados foram coletados por meio de entrevista semiestruturada realizada com 18 usuários em pós-operatório e observação participante no Centro Cirúrgico. Em seguida submetidos à análise de conteúdo de Bardin, emergindo três categorias: A recepção do usuário no Centro Cirúrgico; caracterização da realização do acolhimento na recepção do Centro Cirúrgico na perspectiva do usuário e estratégias de cuidado direcionadas para ambiência, acolhimento e clínica ampliada. Conclui-se que compreender o processo de acolhimento no cotidiano da assistência de enfermagem somente foi possível pelo compartilhamento de experiências de usuários que utilizaram os serviços da unidade. O cuidado de enfermagem neste ambiente foi identificado a partir de duas práxis: na recepção do paciente para cirurgia eletiva e diferentemente para cirurgia de emergência. O ambiente do Centro Cirúrgico gera no usuário uma gama de sentimentos e há um imaginário em torno do evento cirúrgico e deste espaço. No que se refere à diretriz, o cuidado de enfermagem neste setor atende parcialmente ao que esta estabelecido. Um caminho para a viabilização da PNH e da diretriz: acolhimento, ambiência e clínica ampliada é a educação continuada em serviço que deve não somente dispor da política em sua teoria, mas desenvolver métodos para que a torne concreta e palpável promovendo melhoria no cuidado de enfermagem.

Significando a transicionalidade da sexualidade do cônjuge-cuidador da pessoa idosa em processo demencial para um cuidado terapêutico de enfermagem

A sexualidade compreende muitas dimensões da vida dos indivíduos. Ao longo da vida vai sendo revista, à medida que modificações biopsicossociais acontecem e, ao se pensar em relacionamentos conjugais de longa duração é preciso ponderar que estes casais já passaram por transformações na sua relação conjugal e familiar. Para as pessoas idosas o predomínio de doenças crônicas é maior, com risco para incapacidade e/ou dependência, dentre elas a demência. Cônjuges-cuidadores, vivenciando a transicionalidade da sexualidade podem ressignificar a vida, com o apoio do cuidado terapêutico de enfermagem. O estudo teve o objetivo de compreender a vivência da transicionalidade do cônjuge-cuidador da pessoa idosa em processo demencial, para elaboração de um modelo interpretativo de cuidado terapêutico de enfermagem na perspectiva da Teoria das Transições. A fundamentação teórica se baseia nos pressupostos da Teoria das Transições. Estudo de abordagem qualitativa, com base no referencial metodológico da Teoria Fundamentada nos Dados com 25 participantes distribuídos em quatro grupos amostrais (12 cônjuges-cuidadores, 5 filhos e 8 profissionais de saúde). O cenário investigado foi o Núcleo de Atenção ao Idoso, Universidade do Estado do Rio de Janeiro, RJ, Brasil. A coleta dos dados ocorreu entre maio de 2014 e maio de 2015. A técnica utilizada foi à entrevista intensiva e a análise feita mediante codificação inicial, seletiva e focalizada. O projeto de pesquisa foi aprovado pelo Comitê de Ética da UERJ (Processo n 631.538). Os dados demonstraram que a construção da vida conjugal e a história prévia de sexualidade apreendida e vivenciada interferem na maneira de identificar as mudanças provocadas pelo processo demencial e de se adaptar às repercussões para a sexualidade pessoal e conjugal. O fenômeno evidenciado foi a ressignificação da vida do cônjuge-cuidador da pessoa idosa em processo demencial por meio da transicionalidade da sexualidade conjugal, apontando um cuidado terapêutico de enfermagem, sustentado por sete categorias e dezesseis subcategorias, que articuladas, mostram a ressignificação diretamente ligada à história de vida matrimonial, ao engajamento da família como suporte, além do serviço especializado e a disposição em redimensionar a vida sexual consigo e com o outro. Os resultados apontaram o cuidado como mais uma atribuição, com alterações para saúde e em outras dimensões. Por parte dos profissionais, ainda há um despreparo e abordagem muito superficial da sexualidade entre casais que envelhecem, sobremaneira no contexto da demência; para os cônjuges-cuidadores, as crenças e o imaginário social interferem não só no desenvolvimento da sexualidade possível no contexto de vida atual, como na relação de cuidado e na definição do seu papel social; os filhos descrevem o funcionamento familiar na busca da adaptação ao novo contexto de vida dos pais. A ressignificação existe, a partir de estratégias de enfrentamento e da transposição da sexualidade pelo cuidado à pessoa idosa que adoece. Assim, sustenta-se a tese: A compreensão da vivência da transicionalidade da sexualidade do cônjuge-cuidador da pessoa idosa em processo demencial permite a elaboração de um modelo interpretativo que aponta para um cuidado terapêutico de enfermagem próprio para esse momento de vida.

Framework for integration of informal waste management sector with the formal sector in Pakistan.

Historically, waste pickers around the globe have utilised urban solid waste as a principal source of livelihood. Formal waste management sectors usually perceive the informal waste collection/recycling networks as backward, unhygienic and generally incompatible with modern waste management systems. It is proposed here that through careful planning and administration, these seemingly troublesome informal networks can be integrated into formal waste management systems in developing countries, providing mutual benefits. A theoretical framework for integration based on a case study in Lahore, Pakistan, is presented. The proposed solution suggests that the municipal authority should draw up and agree on a formal work contract with the group of waste pickers already operating in the area. The proposed system is assessed using the integration radar framework to classify and analyse possible intervention points between the sectors. The integration of the informal waste workers with the formal waste management sector is not a one dimensional or single step process. An ideal solution might aim for a balanced focus on all four categories of intervention, although this may be influenced by local conditions. Not all the positive benefits will be immediately apparent, but it is expected that as the acceptance of such projects increases over time, the informal recycling economy will financially supplement the formal system in many ways.

Framework for integration of informal waste management sector with the formal sector in Pakistan

Historically, waste pickers around the globe have utilised urban solid waste as a principal source of livelihood. Formal waste management sectors usually perceive the informal waste collection/recycling networks as backward, unhygienic and generally incompatible with modern waste management systems. It is proposed here that through careful planning and administration, these seemingly troublesome informal networks can be integrated into formal waste management systems in developing countries, providing mutual benefits. A theoretical framework for integration based on a case study in Lahore, Pakistan, is presented. The proposed solution suggests that the municipal authority should draw up and agree on a formal work contract with the group of waste pickers already operating in the area. The proposed system is assessed using the integration radar framework to classify and analyse possible intervention points between the sectors. The integration of the informal waste workers with the formal waste management sector is not a one dimensional or single step process. An ideal solution might aim for a balanced focus on all four categories of intervention, although this may be influenced by local conditions. Not all the positive benefits will be immediately apparent, but it is expected that as the acceptance of such projects increases over time, the informal recycling economy will financially supplement the formal system in many ways. © The Author(s) 2013.

Formal specification and refinement of a safe train control function

Motivated by the design and development challenges of the BART case study, an approach for developing and analyzing a formal model for reactive systems is presented. The approach makes use of a domain specific language for specifying control algorithms able to satisfy competing properties such as safety and optimality. The domain language, called SPC, offers several key abstractions such as the state, the profile, and the constraint to facilitate problem specification. Using a high-level program transformation system such as HATS being developed at the University of Nebraska at Omaha, specifications in this modelling language can be transformed to ML code. The resulting executable specification can be further refined by applying generic transformations to the abstractions provided by the domain language. Problem dependent transformations utilizing the domain specific knowledge and properties may also be applied. The result is a significantly more efficient implementation which can be used for simulation and gaining deeper insight into design decisions and various control policies. The correctness of transformations can be established using a rewrite-rule based induction theorem prover Rewrite Rule Laboratory developed at the University of New Mexico.

facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.