Spelling suggestions: "subject:"especificado"" "subject:"especificadas""
31 |
[en] FOMAL ANALYSIS OF PROTOCOLS AND DISTRIBUTED ALGORITHMS: A BASED-LANGUAGE APPROACH / [pt] ANÁLISE FORMAL DE PROTOCOLOS E ALGORITMOS DISTRIBUÍDOS: UMA ABORDAGEM BASEADA EM LINGUAGEMCARLOS BAZILIO MARTINS 03 April 2006 (has links)
[pt] Neste trabalho propomos uma arquitetura para a verificação
formal de protocolos e algoritmos distribuídos. Esta pode
ser vista como uma camada mais abstrata sobre o processo
tradicional de verificação formal, onde temos a
especificação e propriedade a serem verificadas, o
verificador e o resultado retornado por este. O objetivo é
simplificar o processo de especificação e verificação
formal de protocolos e algoritmos distribuídos através de
um ambiente mais dedicado. A parte principal desta
arquitetura é a linguagem de especificação LEP, que contém
construções de domínio-especifíco para simplificar a
especificação destes sistemas. Outra característica desta
linguagem é separar as especificações da topologia e do
protocolo propriamente dito. Acreditamos que esta
separação é válida pois torna mais clara a intenção das
partes e ainda permite, por exemplo, o reuso de uma
topologia entre diferentes especificações de protocolos.
Assim, visamos oferecer uma linguagem cujos exemplos de
especificações devem se assemelhar às descrições de
algoritmos encontradas nos livros didáticos. Além disso,
de forma a se ter a entrada e a saída dos verificadores
formais de forma a obter a saída no nível de abstração de
LEP. / [en] In this work we propose an architecture for the formal
verification of protocols and distribued algoritms. This
can be see as a more abstract layer over the ordinary
process of formal verification, where we have just the
specification of the protocol and properties to be
verified, and the formal tool. Our goal is to simplifu the
specification and formal verification of protocols and
distributed algorithms through a dedicated environment.
The core of the architecture is its input specification
language (Lep), which provides domain-specific
constructions for simplifying the specification of those
systems. With LEP the specification of the protocol and
the specification of the topology to be referred to
protocol are given separetely. We feel that this division
improves the legibility of both and allows the reuse of
the specification of a topology among distinct protocols.
Using this approach we try to offer a language whose
specifications should be similar to the descriptions of
the algorithms found on the didactic books. Moreover, in
order to have the input and output of the architecture
compatible, we also propose a way of processing the result
of the formal verification tool. Then we could have the
result on the abstract level of LEP.
|
32 |
Uma metodologia de modelagem de sistemas computacionais baseada em gramáticas de grafosPretz, Eduardo January 2000 (has links)
Vários métodos de especificação procuram realizar a modelagem de sistemas sob três visões: uma visão funcional, que procura apresentar as informações que trafegam entre os diversos componentes do sistema, uma visão de dados, que apresenta as relações entre as estruturas de dados estáticas do sistema e a visão dinâmica, que mostra as transformações que o sistema pode sofrer ao longo do tempo. Alguns modelos procuram integrar mais de uma visão, mas, em geral, os modelos possuem sérias deficiências ao tentarem representar mais de um aspecto do sistema ao mesmo tempo, sendo necessário o apoio de outros métodos. Este trabalho apresenta um método de especificação de sistemas que procura integrar a modelagem de dados com a modelagem funcional e dinâmica utilizando-se, para isso, das Gramáticas de Grafos como método formal de especificação. Sendo um grafo formado por vértices, arestas e rótulos, pode-se facilmente criar uma camada de abstração em que o usuário (em geral responsável pela análise de sistemas) manipule um método de especificação com o qual já convive, agora com uma semântica formal definida. Espera-se, com a aplicação do método, gerar modelos passíveis de prova, não ambíguos e que promovam um incremento de qualidade no sistema gerado. / Several specification methods try to realize system modeling following three visions: the functional vision, which is based on representing the information exchange among the several components of the system; the data vision, which represents the relations among the static data structures of the system; and the dynamic vision, which presents the transformations the system may endure over the time. Some models exist that try to integrate more than one of these visions, but, in general, they suffer from deficiencies when trying to represent more than one aspect of the system at the same time, in which case the use of other methods is necessary. This work presents a novel method of systems specification that attempts to integrate data modeling with functional and dynamic modelings using, for this, Graph Grammars as its formal specification method. A graph, being made of nodes, edges and labels, is appropriate for creating, easily, an abstraction layer in which the user (usually responsible for the system analysis) manipulates a specification method which is known to him, but now with a well defined formal semantics. We hope, by applying this method, to generate provable, unambiguous models which promote an increase in the quality of the generated system.
|
33 |
Uma metodologia de modelagem de sistemas computacionais baseada em gramáticas de grafosPretz, Eduardo January 2000 (has links)
Vários métodos de especificação procuram realizar a modelagem de sistemas sob três visões: uma visão funcional, que procura apresentar as informações que trafegam entre os diversos componentes do sistema, uma visão de dados, que apresenta as relações entre as estruturas de dados estáticas do sistema e a visão dinâmica, que mostra as transformações que o sistema pode sofrer ao longo do tempo. Alguns modelos procuram integrar mais de uma visão, mas, em geral, os modelos possuem sérias deficiências ao tentarem representar mais de um aspecto do sistema ao mesmo tempo, sendo necessário o apoio de outros métodos. Este trabalho apresenta um método de especificação de sistemas que procura integrar a modelagem de dados com a modelagem funcional e dinâmica utilizando-se, para isso, das Gramáticas de Grafos como método formal de especificação. Sendo um grafo formado por vértices, arestas e rótulos, pode-se facilmente criar uma camada de abstração em que o usuário (em geral responsável pela análise de sistemas) manipule um método de especificação com o qual já convive, agora com uma semântica formal definida. Espera-se, com a aplicação do método, gerar modelos passíveis de prova, não ambíguos e que promovam um incremento de qualidade no sistema gerado. / Several specification methods try to realize system modeling following three visions: the functional vision, which is based on representing the information exchange among the several components of the system; the data vision, which represents the relations among the static data structures of the system; and the dynamic vision, which presents the transformations the system may endure over the time. Some models exist that try to integrate more than one of these visions, but, in general, they suffer from deficiencies when trying to represent more than one aspect of the system at the same time, in which case the use of other methods is necessary. This work presents a novel method of systems specification that attempts to integrate data modeling with functional and dynamic modelings using, for this, Graph Grammars as its formal specification method. A graph, being made of nodes, edges and labels, is appropriate for creating, easily, an abstraction layer in which the user (usually responsible for the system analysis) manipulates a specification method which is known to him, but now with a well defined formal semantics. We hope, by applying this method, to generate provable, unambiguous models which promote an increase in the quality of the generated system.
|
34 |
Uma metodologia de modelagem de sistemas computacionais baseada em gramáticas de grafosPretz, Eduardo January 2000 (has links)
Vários métodos de especificação procuram realizar a modelagem de sistemas sob três visões: uma visão funcional, que procura apresentar as informações que trafegam entre os diversos componentes do sistema, uma visão de dados, que apresenta as relações entre as estruturas de dados estáticas do sistema e a visão dinâmica, que mostra as transformações que o sistema pode sofrer ao longo do tempo. Alguns modelos procuram integrar mais de uma visão, mas, em geral, os modelos possuem sérias deficiências ao tentarem representar mais de um aspecto do sistema ao mesmo tempo, sendo necessário o apoio de outros métodos. Este trabalho apresenta um método de especificação de sistemas que procura integrar a modelagem de dados com a modelagem funcional e dinâmica utilizando-se, para isso, das Gramáticas de Grafos como método formal de especificação. Sendo um grafo formado por vértices, arestas e rótulos, pode-se facilmente criar uma camada de abstração em que o usuário (em geral responsável pela análise de sistemas) manipule um método de especificação com o qual já convive, agora com uma semântica formal definida. Espera-se, com a aplicação do método, gerar modelos passíveis de prova, não ambíguos e que promovam um incremento de qualidade no sistema gerado. / Several specification methods try to realize system modeling following three visions: the functional vision, which is based on representing the information exchange among the several components of the system; the data vision, which represents the relations among the static data structures of the system; and the dynamic vision, which presents the transformations the system may endure over the time. Some models exist that try to integrate more than one of these visions, but, in general, they suffer from deficiencies when trying to represent more than one aspect of the system at the same time, in which case the use of other methods is necessary. This work presents a novel method of systems specification that attempts to integrate data modeling with functional and dynamic modelings using, for this, Graph Grammars as its formal specification method. A graph, being made of nodes, edges and labels, is appropriate for creating, easily, an abstraction layer in which the user (usually responsible for the system analysis) manipulates a specification method which is known to him, but now with a well defined formal semantics. We hope, by applying this method, to generate provable, unambiguous models which promote an increase in the quality of the generated system.
|
35 |
[en] MODELING LEARNING OBJECTS COMPOSITION / [pt] MODELAGEM DE COMPOSIÇÃO DE OBJETOS DE APRENDIZAGEMDIVA DE SOUZA E SILVA 12 July 2006 (has links)
[pt] O desenvolvimento de conteúdos instrucionais utilizando
as novas tecnologias de informação é um processo caro, demorado e
complexo, que aponta para o estabelecimento de novas metodologias. É neste
contexto que surge o conceito de Objeto de Aprendizagem (LO), cujo enfoque
está em promover a
reutilização do conteúdo. Entretanto, ao considerar o
reuso de conteúdo, também
se observa uma necessidade de seqüência - lo para formar
conteúdos mais
elaborados ou mais complexos. Nesta tese adota-se uma
estratégia de representar
LOs cada vez menores, representando separadamente
conteúdo
e prática, aqui
denominados Objetos Componentes (OCs). Para a
estruturação
do conteúdo,
adaptou-se uma proposta já existente e definiu-se um
esquema conceitual
adequado à representação de atividades (ou práticas) de
aprendizagem. Com vista
à composição dos OCs, foi igualmente definido um esquema
conceitual
envolvendo conteúdos e práticas. Assim, com base em um
algoritmo de
seqüenciamento de OCs, um professor pode compreender
melhor a forma de
implementar um objeto complexo, como uma aula ou um
curso,
reduzindo erros e
eventuais omissões na implementação da solução. Este
seqüenciamento deve
seguir uma metodologia e deve ser especificado de modo
não
ambíguo. É neste
contexto que também é apresentada uma linguagem para
especificação de
seqüências de objetos de aprendizagem, com uma sintaxe
adequada à descrição
das possíveis formas de seqüenciamento de LOs.
Finalmente,
descreve-se um
estudo de caso ilustrando a utilização dos esquemas
conceituais desenvolvidos, do
algoritmo proposto e da linguagem de especificação de
seqüências OCs. / [en] The development of instructional content using new
Information
Technologies is an expensive, time-consuming and complex
process that leads to
the development of new methodologies. It was in this
context that the concept of
Learning Objects (LOs) was proposed as an approach that
promotes content reuse.
However, if content is expressed as small LOs, it is also
necessary to sequence
them in order to build more elaborated and complex
content. In this thesis we
adopt a strategy to represent smaller LOs, modeling not
only content but also
practice, called Component Objects (COs) herein. In order
to structure content we
adapted an existing proposal and defined a conceptual
schema to structure
learning practices (or activities). We also defined a
conceptual schema for
composing these COs. Then, based on these conceptual
schemas it was possible to
propose an algorithm for sequencing COs, which supports a
teacher/professor to
better control the implementation of a complex content
such as a class or a course,
thus reducing errors and eventual omissions in its
implementation. The
sequencing process must follow a methodology and must be
specified in a nonambiguous
way. It is in this context that we also present a
specification language
for sequences of LOs, with a syntax that is adequate to
the description of the
possible ways of sequencing LOs. Finally, we describe a
case study that shows the
conceptual schemas that were proposed and the use of the
sequencing algorithm
and the specification language.
|
36 |
Semântica e uma ferramenta para o método SADTRibeiro, Adagenor Lobato January 1991 (has links)
A definição de requisitos tem sido reconhecida como uma das mais críticas e difíceis tarefas em engenharia de software. A necessidade de ferramentas de suporte é essencial. Nos dias de hoje, entre os vários métodos existentes para apoiar a fase de requisitos, destaca-se o SADT (Structured Analysis and Design Techniques) devido a sua capacidade de representar modelos. Este trabalho estabelece semântica para o método SADT, baseando-se na inter-relação do método aos sistemas de fluxo de dados (redes, grafos e máquinas de fluxo). Faz-se, inicialmente, uma abordagem operacional para a semântica de seus construtos básicos e, posteriormente discute-se a possibilidade de executar especificações através de simulação. Uma ferramenta para suportar o método SADT foi projetada e construída e é apresentada. Ela foi definida a partir de um modelo, denotado por uma classe, através de uma sintaxe abstrata. Essa ferramenta foi implementada no ambiente PROSOFT, fornecendo para o usuário mais de quarenta operações de apoio a construção/manipulação de diagramas. O trabalho também apresenta a especificação formal em VDM - Vienna Development Method, da semântica dos principais construtos do método SADT, bem como uma proposição de execução de especificações através de simulação são ainda indicadas direções nas quais o trabalho pode ser estendido. / The definition of systems requirements has been known as one of the most critical and dificult tasks as far as the software engineering is concerned. The need support is essential. Nowadays, among the various methods devised to support the phase of requirements, a special emphasis is given to the SADT method (Structured Analysis and Design Techniques), due to its capability of representing models. This work set semantic for the SADT method, based primarily upon the interrelation of the method to the systems of dataflow (nets, graphs and dataflow machines). It deals with an approach of operational semantics to its basic constructs, and it will, afterwards, discuss the possibility of carry out specifications by simulation. A tool was built to support the SADT method, and it was defined by a model denoted by a class, through an abstract syntax. This tool was implemented in the PROSOFT environment, providing for the user, more than forty support operations for the construction /manipulation of diagrams. This work also presents the formal specification of the semantics of the main constructs of the SADT method in VDM - Vienna Development Method; as well as an execution proposal of specifications through simulation. Directions have been indicated concerning the extension of the research.
|
37 |
Uma linguagem comum entre usuários e analistas para definição de requisitos de sistemas de informaçãoLoh, Stanley January 1991 (has links)
O presente trabalho tem por objetivo apresentar uma linguagem comum entre Usuários e Analistas para definição de requisitos, a ser utilizada durante as fases de Análise de Requisitos e Especificação, realizadas durante o desenvolvimento de Sistemas de Informação. A motivação para o trabalho surgiu da busca de uma solução para o problema de compatibilizar as diferenças entre as linguagens usadas por aqueles. Normalmente, são utilizados dois tipos de linguagens. O primeiro tipo tem, por principal característica, a informalidade, sendo as linguagens deste tipo, portanto, naturais mas pouco precisas. Já as linguagens do segundo tipo apresentam grande precisão, mas pouca legibilidade. Considerando que as linguagens informais são melhores para a participação dos Usuários no desenvolvimento de Sistemas de Informação e que as linguagens formais são úteis e necessárias para que Analistas elaborem a especificação do sistema e projetistas a interpretem, fez-se necessário o estudo de uma linguagem intermediária que busque um meio termo entre legibilidade (ou naturalidade) e precisão e que, ao mesmo tempo, seja próxima das linguagens informais e formais já em uso. São também apresentadas, neste trabalho, heurísticas (regras informais) para as transformações entre as linguagens, para justificar a referida proximidade, e um estudo de caso para avaliação dos graus de precisão e legibilidade da linguagem comum proposta. / The objecive of this work is to present a common language for users and analists, for requirements definition during Information Systems development. The motivation for this work arose from the study of the communication problem that users and analists have, working with diferent languages of at least two kinds (natural and formal). Natural languages have informality as their main characteristic, hence are not precise. On the other side, formal languages are precise, but sometimes not readable. Informal or natural languages are better for user participation in information system development, and formal languages are useful and necessary to analists when they create a system specification for implementors. It is necessary to search for an intermediate language, that could play a middle role between readableness and precision, and that, at the same time, is relatively close to informal and formal languages. In this work, heuristics (informal and common sense rules) for requirements ellicitation and for transformations between languages are defined too. A case study is detailed, for illustrate the degree of precision and readableness of the common language proposed here.
|
38 |
Semântica e uma ferramenta para o método SADTRibeiro, Adagenor Lobato January 1991 (has links)
A definição de requisitos tem sido reconhecida como uma das mais críticas e difíceis tarefas em engenharia de software. A necessidade de ferramentas de suporte é essencial. Nos dias de hoje, entre os vários métodos existentes para apoiar a fase de requisitos, destaca-se o SADT (Structured Analysis and Design Techniques) devido a sua capacidade de representar modelos. Este trabalho estabelece semântica para o método SADT, baseando-se na inter-relação do método aos sistemas de fluxo de dados (redes, grafos e máquinas de fluxo). Faz-se, inicialmente, uma abordagem operacional para a semântica de seus construtos básicos e, posteriormente discute-se a possibilidade de executar especificações através de simulação. Uma ferramenta para suportar o método SADT foi projetada e construída e é apresentada. Ela foi definida a partir de um modelo, denotado por uma classe, através de uma sintaxe abstrata. Essa ferramenta foi implementada no ambiente PROSOFT, fornecendo para o usuário mais de quarenta operações de apoio a construção/manipulação de diagramas. O trabalho também apresenta a especificação formal em VDM - Vienna Development Method, da semântica dos principais construtos do método SADT, bem como uma proposição de execução de especificações através de simulação são ainda indicadas direções nas quais o trabalho pode ser estendido. / The definition of systems requirements has been known as one of the most critical and dificult tasks as far as the software engineering is concerned. The need support is essential. Nowadays, among the various methods devised to support the phase of requirements, a special emphasis is given to the SADT method (Structured Analysis and Design Techniques), due to its capability of representing models. This work set semantic for the SADT method, based primarily upon the interrelation of the method to the systems of dataflow (nets, graphs and dataflow machines). It deals with an approach of operational semantics to its basic constructs, and it will, afterwards, discuss the possibility of carry out specifications by simulation. A tool was built to support the SADT method, and it was defined by a model denoted by a class, through an abstract syntax. This tool was implemented in the PROSOFT environment, providing for the user, more than forty support operations for the construction /manipulation of diagrams. This work also presents the formal specification of the semantics of the main constructs of the SADT method in VDM - Vienna Development Method; as well as an execution proposal of specifications through simulation. Directions have been indicated concerning the extension of the research.
|
39 |
Uma linguagem comum entre usuários e analistas para definição de requisitos de sistemas de informaçãoLoh, Stanley January 1991 (has links)
O presente trabalho tem por objetivo apresentar uma linguagem comum entre Usuários e Analistas para definição de requisitos, a ser utilizada durante as fases de Análise de Requisitos e Especificação, realizadas durante o desenvolvimento de Sistemas de Informação. A motivação para o trabalho surgiu da busca de uma solução para o problema de compatibilizar as diferenças entre as linguagens usadas por aqueles. Normalmente, são utilizados dois tipos de linguagens. O primeiro tipo tem, por principal característica, a informalidade, sendo as linguagens deste tipo, portanto, naturais mas pouco precisas. Já as linguagens do segundo tipo apresentam grande precisão, mas pouca legibilidade. Considerando que as linguagens informais são melhores para a participação dos Usuários no desenvolvimento de Sistemas de Informação e que as linguagens formais são úteis e necessárias para que Analistas elaborem a especificação do sistema e projetistas a interpretem, fez-se necessário o estudo de uma linguagem intermediária que busque um meio termo entre legibilidade (ou naturalidade) e precisão e que, ao mesmo tempo, seja próxima das linguagens informais e formais já em uso. São também apresentadas, neste trabalho, heurísticas (regras informais) para as transformações entre as linguagens, para justificar a referida proximidade, e um estudo de caso para avaliação dos graus de precisão e legibilidade da linguagem comum proposta. / The objecive of this work is to present a common language for users and analists, for requirements definition during Information Systems development. The motivation for this work arose from the study of the communication problem that users and analists have, working with diferent languages of at least two kinds (natural and formal). Natural languages have informality as their main characteristic, hence are not precise. On the other side, formal languages are precise, but sometimes not readable. Informal or natural languages are better for user participation in information system development, and formal languages are useful and necessary to analists when they create a system specification for implementors. It is necessary to search for an intermediate language, that could play a middle role between readableness and precision, and that, at the same time, is relatively close to informal and formal languages. In this work, heuristics (informal and common sense rules) for requirements ellicitation and for transformations between languages are defined too. A case study is detailed, for illustrate the degree of precision and readableness of the common language proposed here.
|
40 |
[en] A GRAPH BASED THEOREM PROVING PLATFORM WITH STRATEGIES / [pt] UMA PLATAFORMA DE DEMONSTRAÇÃO DE TEOREMAS BASEADA EM GRAFOSBRUNO SCHROEDER 09 February 2017 (has links)
[pt] Demonstrações em lógica podem tornar-se muito grandes e complexas. Para
resolver problemas, e para estudar lógica, é comum valer-se de assistentes de
demonstração. Um assistente de demonstração geral deve integrar ferramentas que
ajudem a especificar as lógicas, as equações, os conjuntos de regras, e as
estratégias de busca (semi) automática de demonstrações. A comunidade usuária
de Provadores Automáticos de Teoremas conhece algumas ferramentas que
atendem a estes requisitos. Entretanto, estas ferramentas não estão preparadas para
lidar com demonstrações muito grandes. Trabalhos recentes sugerem que uma boa
forma de chegar a demonstrações menores é usar grafos, ao invés de árvores, para
representar demonstrações. Esta dissertação descreve e implementa uma máquina
virtual baseada em grafo e um compilador para a confecção de provadores de
teoremas baseados em grafo. Para validar a ferramenta, alguns estudos de casos e
provadores de teoremas baseados em grafo são apresentados. / [en] Proofs in logic can become very big and complex. For problem solving, and
to teach logic, it is common the use of proof assistants. A general proof assistant
should integrate tools to help users on specifying the logics, the formulas, the sets
of rules, and the very strategy to perform (semi) automatic proof search. The
Automatic Theorem Provers community is aware of some tools that were
designed to fulfill these requirements. However, these tools do not take the
(possibly) huge size of a proof. Recent works have pointed out that a good way to
achieve shorter proofs is the use of graphs, instead of trees, to represent proofs.
This dissertation describes and implements a graph-based virtual machine and a
compiler for the production of graph-based theorem provers. Some case studies,
standard as well as graph-based theorem prover, are illustrated in order to validate
the tool.
|
Page generated in 0.0791 seconds