Spelling suggestions: "subject:"modelos formais"" "subject:"odelos formais""
1 |
A representação social da teoria de Piaget no Brasil: implicações para as pesquisas acadêmicas / The social representation of Piaget\'s theory in Brazil: implications to the academic researchesMarçal, Vicente Eduardo Ribeiro 07 June 2019 (has links)
O objetivo desta Tese foi o de demonstrar que a Teoria do biólogo e epistemólogo suíço Jean Piaget foi vítima de sua própria Representação Social, (na acepção de Serge Moscovici, como explicitaremos já em nossa Introdução). Vítima no sentido de que suas descobertas na área da Biologia e sua criação no campo da construção de modelos formais na mesma ciência, feito inédito até então, caíram no ostracismo na História da ontogênese epigenética do ser humano, tanto nos aspectos biológicos, quanto na área da aquisição do conhecimento científico e lógico matemático. Esses fatos nos mostram Zelia Ramozzi-Chiarottino, (cuja análise e interpretação da Teoria de Jean Piaget constituir-se-á no referencial teórico desta Tese) ao lado de seus colaboradores, no artigo: Jean Piagets unrecognized epigenetic ontogenesis of the logical mathematical thought, (2017). Neste trabalho, restringimo-nos ao Brasil e à produção de Dissertações e Teses de Doutorado sobre a Teoria de Piaget e sua representação social, aqui realizadas nos últimos dez anos. Fizemos um levantamento das Dissertações e Teses a partir do Catálogo de Teses e Dissertações da CAPES. O método estatístico que utilizamos foi o do para analisar os dados coletados. Esta análise confirmou nossa conjectura / Our aim with this Ph.D Thesis was to demonstrate that the Theory of the swiss biologist and epistemologist Jean Piaget was victim of its own Social Representation (within the meaning of Serge Moscovici, as we will still explain in our Introduction). Victim in sense of that his findings in the field of Biology and his creation in the field of the construction of formal models in this same Science, unprecedent feat till then, have fallen in obscurity in the History of epigenetic ontogenesis of the human being, in both biologic and scientific aspects, in terms of the field of acquiring of scientific and logical mathematical knowledgement. These facts Zelia Ramozzi-Chiarottino (whose analysis and interpretation of Piagets Theory will be the theoretical framework of this Thesis) show us next to her co-workers, in the article: Jean Piagets unrecognized epigenetic ontogenesis of the logical mathematical thought, (2017). In the present work, we limited ourselves to Brazil, and to the production of Dissertations and Doctoral Theses on Piagets Theory and its Social Representation, produced here on the last ten years. We made a data survey on the Dissertations and Theses from the Catalogue of Theses and Dissertations from CAPES. Statistic method used was the to analyze the collected data. This analysis validated our conjecture
|
2 |
Geração de especificação formal de sistemas a partir de documento de requisitosda Fonseca Limaverde Cabral, Gustavo January 2007 (has links)
Made available in DSpace on 2014-06-12T15:59:36Z (GMT). No. of bitstreams: 2
arquivo5340_1.pdf: 1555764 bytes, checksum: d3735403fc535c9dd852536b0afde205 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2007 / A escrita de requisitos, dentro do processo de desenvolvimento de sistemas, está sujeita a falhas,
uma vez que os requisitos são escritos em Linguagem Natural, como Inglês, que pode conter
definições ambíguas ou de difícil entendimento. Por outro lado, Linguagem Natural é a opção
mais simples e flexível para se especificar um sistema, e é a linguagem de entendimento comum
entre clientes e contratados. Desta forma, para minimizar a existência de erros nos documentos
de requisitos, técnicas de validação com inspeção ou revisão de documentos são utilizadas.
Entretanto, o custo de se realizar este tipo de validação é alto e sua eficácia é questionável;
erros podem persistir. Além disso, requisitos escritos usando de linguagem natural são de
difícil processamento, dificultando a geração de outros artefatos a partir do mesmo.
Esta dissertação define uma estratégia que utiliza templates de especificação de casos de
use e uma Linguagem Natural Controlada (LNC) para descrever requisitos. Os templates de
casos de uso asseguram a estruturação correta do documento de requisitos e a LNC garante
a exatidão da gramática do texto que especifica o comportamento do sistema. Foram criados
dois templates de casos de uso, cada um com uma visão diferente do sistema. A visão mais
abstrata se chama visão do usuário e a visão mais detalhada se chama visão de componentes.
A partir dessa estruturação dos requisitos torna-se, possível definir uma estratégia de geração
automática de uma especificação formal da aplicação em questão.
A geração automática de especificação formal de sistemas reduz custo e necessidade de
mão de obra especializada em projetos de desenvolvimento de software. Ou seja, uma vez que
é possível realizar a geração automática do modelo formal de sistemas podemos fazer uso do
mesmo na validação de propriedades do sistema. Além disso, artefatos como casos de teste e
diagramas UML podem ser gerados a partir deste. Em particular, esta dissertação define uma
estratégia para gerar modelos formais na álgebra de processo CSP a partir das duas visões de
caso de uso, mantendo a consistência entre os artefatos. Também foi definida uma relação de
refinamento entre os modelos gerados garantindo a consistência entre as visões.
Finalmente, todo o processo foi automatizado através de ferramentas. Estas foram vali-
dadas através de experimentos realizados no contexto de aplicação para celulares da Motorola,
empresa parceira e financiadora do projeto de pesquisa com o CIn/UFPE
|
3 |
Modelling and Integrating Formal Models: from Test Cases and Requirements ModelsSOUZA, Cléclio Feitosa de January 2007 (has links)
Made available in DSpace on 2014-06-12T15:59:48Z (GMT). No. of bitstreams: 1
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2007 / A especificação formal de um sistema ou seu modelo formal é uma forma abstrata de representar
suas propriedades (características). Métodos formais é um ramo da Engenharia de Software
com foco no desenvolvimento de sistemas tendo uma especificação formal do mesmo como
ponto de partida. Inicialmente, as vantagens de usar notações abstratas antes da implementação
do sistema estavam apenas relacionadas a um melhor entendimento do problema. Depois,
tornou-se evidente que o uso de notações formais abstratas combinadas com técnicas de refinamentos
de modelos reduzem o tempo de desenvolvimento e aumentam a qualidade do produto
de sistema.
A fase de testes é positivamente influenciada pelo uso de métodos formais. Pesquisas têm
sido desenvolvidas para melhorar a qualidade do sistema usando modelos formais e casos de
teste. Uma vez verificadas as propriedades do sistema através de uma investigação dos modelos
formais, é possível gerar casos de testes confiáveis do sistema que serão colocados em ação
para verificar a implementação do sistema posteriormente. O campo de pesquisa que explora
métodos formais aplicados com testes de software é chamada de Testes Baseados em Modelos,
ou simplesmente MBT, do inglês Model-Based Testing.
Porém, há situações onde não é possível possuir o modelo abstrato definido a priori. Para
superar tal restrição outras técnicas surgiram para sintetizar um modelo abstrato seguindo apenas
execuções do sistema. As execuções de um sistema contêm comportamentos necessários
para construir um modelo abstrato desse sistema. Na literatura atual, tais técnicas usadas para
construir representações abstratas seguindo execuções do sistema são chamadas de Anti-Model-
Based Testing ou simplesmented Anti-MBT. Então, depois de construir um modelo abstrato,
técnicas de verificação de modelos e geração de casos de teste seguindo modelos formais podem
ser aplicadas normalmente.
O propósito desse trabalho é dar suporte a algumas técnicas de MBT usadas no contexto
da Motorola (CIn/BTC). Em tais técnicas, as especificações usadas para gerar casos de testes
são geralmente incompletas, inconsistentes, e às vezes não existem. Portanto, usando casos de
testes reais do sistema é possível criar novas especificações e atualizar especificações originais
do sistema, e posteriormente gerar novos casos de teste usando comportamentos válidos do
sistema. Um outro problema detectado em nosso contexto é a distância existente entre as
representações abstratas e reais. Um caso de teste abstrato, por exemplo, é útil em técnicas
formais, mas não é possível executar um caso de teste diretamente no sistema. Dessa forma,
para executar (manualmente ou automaticamente) os casos de teste gerados pelas técnicas de
MBT é necessário primeiro traduzi-los em uma representação real.
Como resultado desse trabalho nós desenvolvemos técnicas formais de modelagem do comportamento
do sistema usando casos de teste. Os resultados das técnicas de modelagem são modelos formais especificados nos formalismos de LTS ou CSP. Além disso, nós definimos
uma técnica de unificação que une modelos formais gerados a partir de diferentes artefatos do
sistema (requisitos e casos de teste). O resultado da técnica de unificação é um completo e
unificado modelo do sistema, que contém informações providas de diferentes artefatos. Nós
também definimos uma técnica para traduzir casos de teste abstratos em representações reais.
Os casos de teste reais gerados por nossa técnica de tradução são usados no contexto do time de
automação de testes da Motorola, onde esse trabalho está inserido. Finalmente, nós automatizamos
as técnicas desenvolvidas usando linguagens de programação e especificações formais.
O resultado é a ferramenta TCRev que é capaz de modelar, unificar e traduzir modelos do
sistema.
A ferramenta TCRev interage com o outras ferramentas externas, tais como FDR e FDR Explorer.
Todos os resultados foram validados em estudos de casos reais executados no contexto
da Motorola. Nessa dissertação nós apresentamos um destes estudo de casos
|
4 |
Modelagem e verificação automática de um protocolo de controle de fluxo adaptativo usando traços de execução.MOREIRA, Anne Lorayne Gerônimo Silva Augusto. 22 May 2018 (has links)
Submitted by Maria Medeiros (maria.dilva1@ufcg.edu.br) on 2018-05-22T14:55:43Z
No. of bitstreams: 1
ANNE LORAYNE GERÕNIMO SILVA AUGUSTO MOREIRA - DISSERTAÇÃO (PPGCC) 2016.pdf: 843001 bytes, checksum: 3c03d468b4f80d420da1bad90adf7ca0 (MD5) / Made available in DSpace on 2018-05-22T14:55:43Z (GMT). No. of bitstreams: 1
ANNE LORAYNE GERÕNIMO SILVA AUGUSTO MOREIRA - DISSERTAÇÃO (PPGCC) 2016.pdf: 843001 bytes, checksum: 3c03d468b4f80d420da1bad90adf7ca0 (MD5)
Previous issue date: 2016 / Capes / O desenvolvimento de sistemas embarcados possibilitou uma forte expansão no número de aplicações dependentes de dispositivos programáveis em áreas tão distintas como automobilística, sistemas financeiros e sistemas médicos. Uma eventual falha em algum desses sistemas pode provocar diferentes graus de danos e prejuízos e, por isso, exige-se um alto grau de confiabilidade em seu funcionamento. O aumento da complexidade dos novos sistemas computacionais e a pressão econômica e busca de novos mercados, concorrem para a busca da redução nos prazos de entrega dos dispositivos programáveis e de seus softwares e sistemas embarcados. Este trabalho apresenta um estudo de caso para a utilização de um método de verificação formal de software aplicado a um sistema computacional de controle de fluxo adaptativo para Gateways Bluetooth Low-Energy utilizados em sistemas de monitoramento remoto de pacientes. Os resultados obtidos neste trabalho confirmam a viabilidade da aplicação do método na verificação formal do software proposto. / The embedded system development had a positive impact on the expansion of applications dependent on programmable devices inside many areas such as automotive industry, financial services, and medical systems. A failure in any of these systems can cause losses and damages on many levels. Therefore, embedded systems require a high level of reliability while operating. The increasing complexity of these new computational systems, the cost-effective pressure, and the new market demand, contribute to reduce the delivery deadlines of the programmable devices, their softwares, and embedded systems. This research presents a case study in which we evaluated the usage of a formal verification method applied to a computational controlling system, with adaptive flow, for Gateway Bluetooth Low Energy used in patient monitoring systems. The results obtained in this study confirm the application feasibility of the formal verification method of the proposed software.
|
5 |
Teoria da escolha pública: uma introdução crítica / Public choice theory: a critical introductionBernabel, Rodolpho Talaisys 02 July 2009 (has links)
Reconstruímos a Teoria da Escolha Pública explicitando seus pressupostos sobre a natureza do objeto, do conhecimento e dos valores e sua lógica de operação, ou seja, seu método de solução de problemas. Mostramos com essa teoria que podemos entender a política como um processo de pacificação pela troca, em vez de um processo de pacificação pelo poder. Temos então novas respostas para as perguntas fundamentais da Ciência Política: Como é possível emergir a cooperação pacífica e legítima entre indivíduos? Qual é a maneira de fazer com que diferentes interesses individuais sejam reconciliados? A Teoria sugere que a política pode ser um jogo de soma positiva, evitando deseconomias constitucionais, guiando-se pelo princípio da unanimidade. Mostraremos então os desenhos constitucionais como ambientes de interação entre indivíduos e poderemos predizer que regras engendrarão cooperação ou competição. / We do a reconstruction of the Public Choice Theory explaining their assumptions about the nature of the object, knowledge and values and logic of their operation, i.e. its method of solution of problems. We show that with this theory we can understand the politics as a process of pacification through trade-offs, instead of a peace process by means of power. Proceeding in this way we obtain new answers to fundamental questions of Political Science: How can emerge a peaceful and legitimate cooperation among individuals? What is the way to conciliate different individual interests? The theory suggests that politics can be a positive-sum game, avoiding constitutional diseconomies, and must be guided by the principle of unanimity. Then we show how the constitutional designs as interaction environments for individuals and so can predict what rules make cooperation or competition.
|
6 |
Teoria da escolha pública: uma introdução crítica / Public choice theory: a critical introductionRodolpho Talaisys Bernabel 02 July 2009 (has links)
Reconstruímos a Teoria da Escolha Pública explicitando seus pressupostos sobre a natureza do objeto, do conhecimento e dos valores e sua lógica de operação, ou seja, seu método de solução de problemas. Mostramos com essa teoria que podemos entender a política como um processo de pacificação pela troca, em vez de um processo de pacificação pelo poder. Temos então novas respostas para as perguntas fundamentais da Ciência Política: Como é possível emergir a cooperação pacífica e legítima entre indivíduos? Qual é a maneira de fazer com que diferentes interesses individuais sejam reconciliados? A Teoria sugere que a política pode ser um jogo de soma positiva, evitando deseconomias constitucionais, guiando-se pelo princípio da unanimidade. Mostraremos então os desenhos constitucionais como ambientes de interação entre indivíduos e poderemos predizer que regras engendrarão cooperação ou competição. / We do a reconstruction of the Public Choice Theory explaining their assumptions about the nature of the object, knowledge and values and logic of their operation, i.e. its method of solution of problems. We show that with this theory we can understand the politics as a process of pacification through trade-offs, instead of a peace process by means of power. Proceeding in this way we obtain new answers to fundamental questions of Political Science: How can emerge a peaceful and legitimate cooperation among individuals? What is the way to conciliate different individual interests? The theory suggests that politics can be a positive-sum game, avoiding constitutional diseconomies, and must be guided by the principle of unanimity. Then we show how the constitutional designs as interaction environments for individuals and so can predict what rules make cooperation or competition.
|
7 |
[pt] FINALIZADORES E REFERÊNCIAS FRACAS: INTERAGINDO COM O COLETOR DE LIXO / [en] FINALIZERS AND WEAK REFERENCES: INTERFACING WITH THE GARBAGE COLLECTORMARCUS AMORIM LEAL 03 January 2006 (has links)
[pt] Inúmeras linguagens de programação oferecem suporte a
finalizadores e referências fracas. Não obstante, de
maneira geral esses mecanismos são relativamente
pouco conhecidos e pouco usados por programadores. Mesmo
entre pesquisadores e desenvolvedores de linguagens não
existe muito consenso
quanto à sua semântica, que varia consideravelmente entre
diferentes
implementações. Neste trabalho buscamos explorar os
conceitos de finalizadores
e de referências fracas, suprindo a ausência de uma
especificação clara
e abrangente, e permitindo uma melhor compreensão,
implementação e uso
dos mecanismos correspondentes. Como ponto de partida
realizamos um
amplo levantamento sobre como é feito o suporte a
finalizadores e referências
fracas em diferentes linguagens de programação,
identificando as características comuns, os problemas, e
as questões semânticas mais relevantes associadas
às implementações consideradas. Para garantir uma maior
precisão
em nossa análise, utilizamos um modelo abstrato de uma
linguagem de programação com gerenciamento automático de
memória. Através deste modelo
especificamos formalmente a semântica de finalizadores e
referências fracas,
incluindo descrições das suas principais variantes e
mecanismos relacionados.
Além disso, provamos certas propriedades inerentes a
linguagens de
programação com gerenciamento automático de memória,
indicando como
estas são afetadas pela introdução de finalizadores e
referências fracas. Por
fim, consideramos possíveis estratégias de implementação
desses mecanismos
em diferentes tipos de sistemas. Algumas das opções
semânticas investigadas
impõe um custo de processamento expressivo, o que
frequentemente
inviabiliza a sua adoção na prática. / [en] Most mainstream programming languages support finalizers
and weak
references. In spite of that, these abstractions are still
modestly known
by programmers in general. Even among language designers
there seems
to be no common view on how to define their semantics, and
language
implementations certainly reflect that. In this thesis we
explore the concepts
of finalizer and weak reference by discussing several
important issues that, as
far as we know, have not been explored by other authors.
After presenting
a survey on how finalizers and weak references are
supported by actual
programming languages, we thoroughly examine their
semantics and discuss
alternative implementation strategies. We also use an
operational approach
to develop a formal model for reasoning about garbage
collection and its
interaction with client programs. By explicitly
representing low-level details,
such as heap memory and its addresses, we were able to
clearly specify
memory management actions, and prove several important
memory-related
language invariants. Using this model we describe a formal
semantics for
finalizers and weak references, exploring some of its many
subtleties. We
believe that the topics covered here can serve as a
relevant reference for
further investigations, and also help to guide actual
implementations.
|
8 |
Uso de modelos formais em sistemas pervasivos de cuidados de saúde: um estudo de caso em auxílio à prática de exercícios físicos. / Use of formal models in pervasive health care systems: a case study to aid in the practice of physical exercises.OLIVEIRA, Elthon Allex da Silva. 04 May 2018 (has links)
Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-05-04T23:12:17Z
No. of bitstreams: 1
ELTHON ALEX DA SILVA OLIVEIRA - TESE PPGCC 2015..pdf: 4180608 bytes, checksum: 808dd922bbed2d1a31a83917caaf05c5 (MD5) / Made available in DSpace on 2018-05-04T23:12:17Z (GMT). No. of bitstreams: 1
ELTHON ALEX DA SILVA OLIVEIRA - TESE PPGCC 2015..pdf: 4180608 bytes, checksum: 808dd922bbed2d1a31a83917caaf05c5 (MD5)
Previous issue date: 2015-05-08 / Diversas soluções de software têm sido desenvolvidas para a área de cuidados de saúde. Nesta área, destacam-se as pesquisas em exercícios físicos, que tem recebido grande atenção da Organização Mundial de Saúde por ajudar a diminuir os riscos de diversas doenças e a aumentar a qualidade de vida das pessoas acometidas por alguma delas. Contudo, há três problemas principais nas soluções existentes desenvolvidas para o acompanhamento de exercícios físicos: i) levam em consideração apenas variáveis fisiológicas, ii) necessitam da atenção do profissional de saúde durante a prática do exercício e iii) não fornecem recomendações customizadas. Neste trabalho, é apresentado um método para proporcionar a manutenção de conformidade entre as ações dos indivíduos e as recomendações do profissional de saúde, durante a prática de exercícios, sem a presença do mesmo in loco. Tal método possibilita a construção de um modelo na forma de autômato finito. Este autômato, chamado de modelo de referência, é capaz de descrever como o indivíduo deve se comportar a fim de se manter em conformidade com as recomendações do profissional de saúde. Por ser gerado a partir da composição de modelos menores, a evolução do modelo pode ser obtida
e as propriedades garantidas por construção. Além disso, propriedades de vivacidade e
segurança são verificadas no modelo construído por meio da técnica de verificação de modelos, fornecendo confiabilidade ao sistema. Algumas tarefas foram executadas no processo de avaliação do método apresentado e demonstraram que: o processo de construção do modelo de referência está de acordo com o processo clínico; o modelo gerado é capaz de representar o conhecimento do especialista, fornecendo recomendações adequadas ao indivíduo; e a solução apresentada é tecnicamente viável de se implementada e executada; e,por fim,este método pode ser usado em cenários reais,desde que os indivíduos não estejam sob condições de estresse. / Several software solutions have been developed for the healthcare area. In this area, we
high light the area of physical exercise that has received great attention from World Health Organization for helping decreasing risk of various diseases and improving the quality of life of people affected by some of them. However, there are three main problems with such solutions developed for monitoring of physical exercises: i) only physiological variables are supported, ii) professional attention is required during the exercise, and iii) customized recommendations are not given. In this work,we present a method to provide accordance maintenance between individuals actions and recommendations from health care professional, during the exercise execution, without the presence of himin loco. Such a method makes it possible to build a finite automaton model. Such an automaton, called reference model, describes how an individual must behave aiming to follow recommendations from the health care professional. As it is obtained by means of composition from smaller models, the model evolution is accomplished and properties are guaranteed by means of building process. Besides, liveness and safety properties are checked in the model by the model checking technique,making the model more reliable. Some tasks were performed during the evaluation process and showed that: the building process of the reference model is according to the clinical procedure; the generated reference model is able to represent the knowledge of the health care professional
by providing appropriate recommendations; the presented solution is technically feasible to
be developed and executed; and such a method can be used in real scenarios, since individuals are not under stress conditions.
|
Page generated in 0.062 seconds