1 |
Extração automática de modelos CSP a partir de casos de usoARAÚJO, Renata Bezerra e Silva de 31 January 2011 (has links)
Made available in DSpace on 2014-06-12T16:00:36Z (GMT). No. of bitstreams: 2
arquivo6806_1.pdf: 3125791 bytes, checksum: d312e759783582d509c1403b479df91e (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2011 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / No ciclo de vida de desenvolvimento de software, especificação de requisitos é uma atividade
muito propensa a definições incorretas. Isto geralmente acontece porque esses documentos são
normalmente escritos em linguagem natural, tornando muito alta a possibilidade de introduzir
ambiguidades e interpretações errôneas. Por outro lado, a utilização de linguagem natural traz
simplicidade e flexibilidade ao se especificar requisitos, considerando que esta é uma notação
que pode ser compreendida tanto pelo cliente quanto pelo desenvolvedor.
Uma vez que projetos de software possuem documentos precisos, engenheiros de software
que tenham bom conhecimento em linguagens formais podem criar manualmente uma especificação
formal com o propósito de validar as propriedades do sistema. No entanto, esta criação
manual pode não cobrir todos os requisitos ou podem conter inconsistências. Desta forma, a
geração automática de modelos formais a partir de documento de requisitos parece ser uma boa
solução para este problema. Para alcançar este objetivo, os documentos de requisitos devem ser
simples, diretos, uniformes e sem ambuiguidades. Para que isto aconteça, Linguagens Naturais
Controladas (Controlled Natural Languages - CNL) são comumente utilizadas.
Este trabalho faz parte do projeto de Pesquisa e Desenvolvimento do CIn Brazil Test Center
(CInBTCRD), que é uma cooperação entre a Motorola e o Centro de Informática da Universidade
Federal de Pernambuco (CIn-UFPE). Em primeiro lugar, este trabalho propõe uma
linguagem restrita (CNL) para definir casos de uso contendo uma noção de estado, os quais
consideram dados de entrada, saída, guarda e atualização de variáveis, como um complemento
para a descrição textual. Depois disso, uma tradução automática dessa linguagem para a algebra
de processos CSP foi proposta, a fim de permitir a análise formal de requisitos e geração de
casos de teste. Finalmente, foi realizada a implementação e integração desta linguagem e sua
tradução para CSP em uma ferramenta conhecida como TaRGeT, cujo propósito é a geração
de casos de teste a partir de documentos de casos de uso que seguem um template padrão e
são escritos utilizando uma CNL. A TaRGeT original não era capaz de lidar com definições
de dados e as manipulações destes dados, e utiliza sistemas rotulados por transição (labelled
transition systems) em vez de CSP, como formalismo.
Para ilustrar as técnicas propostas neste trabalho, um estudo de caso foi realizado no ambiente
da Motorola, adaptando um exemplo de caso de uso real da indústria de modo a encaixá-lo
no nosso template. O documento de caso de uso considera situações de envio e recebimento de
SMS/MMS, contendo uma feature com 7 casos de uso, incluindo definições e manipulações de
dados, relacionamentos entre casos de uso e 6 fluxos alternativos. O CSP gerado contém 570
linhas de código e a verificação de suas propriedades foi checada com sucesso utilizando-se a
ferramenta FDR, um verificador de modelo para CSP
|
2 |
Estudo sobre critérios para a especificação de transformadores elevadores de estações geradoras (\"generator step-up transformers\"). / Generator step up transformers - specification.Amaral, Nádia Bentz de Souza 13 April 2007 (has links)
Esse trabalho mostra alguns aspectos construtivos e de sistema que devem fazer parte do projeto e da especificação de um transformador elevador, também conhecido na literatura como generator step-up transformer. O projeto do equipamento é baseado em sua especificação técnica. No entanto, algumas vezes observa-se que a especificação técnica não contempla alguns pontos de extrema importância e que poderão ser cruciais para o bom desempenho do transformador quando em serviço. Transformadores elevadores estão sujeitos a distúrbios do sistema onde operam. O efeito desses distúrbios no equipamento pode ser atenuado através de uma especificação técnica que seja a mais completa possível, no sentido de fornecer informações a respeito do sistema e conexão do transformador tanto ao gerador quanto à rede elétrica; por parte do fabricante cabe o trabalho de interpretar a especificação do equipamento, a fim de projetar um equipamento que opere de forma satisfatória face aos requisitos especificados. / This work presents some constructive and operational aspects that should be take into account on the transformer design and specification. The design of the equipment is based on its technical specification. However, sometimes, it is observed that the technical specification does not contemplate some important points which could be crucial for the good transformer performance when in service. Generator step-up transformers are subject to some system disturbance where they are connected. The effect of these disturbances on the equipment could be minimize with a technical specification as complete as possible, on the sense of provide information regarding the network and connections between generator and power transformer. On the other hand, the manufacturer has the responsibility to interpret the technical requirements in order to design an equipment that operates satisfactory.
|
3 |
Estudo sobre critérios para a especificação de transformadores elevadores de estações geradoras (\"generator step-up transformers\"). / Generator step up transformers - specification.Nádia Bentz de Souza Amaral 13 April 2007 (has links)
Esse trabalho mostra alguns aspectos construtivos e de sistema que devem fazer parte do projeto e da especificação de um transformador elevador, também conhecido na literatura como generator step-up transformer. O projeto do equipamento é baseado em sua especificação técnica. No entanto, algumas vezes observa-se que a especificação técnica não contempla alguns pontos de extrema importância e que poderão ser cruciais para o bom desempenho do transformador quando em serviço. Transformadores elevadores estão sujeitos a distúrbios do sistema onde operam. O efeito desses distúrbios no equipamento pode ser atenuado através de uma especificação técnica que seja a mais completa possível, no sentido de fornecer informações a respeito do sistema e conexão do transformador tanto ao gerador quanto à rede elétrica; por parte do fabricante cabe o trabalho de interpretar a especificação do equipamento, a fim de projetar um equipamento que opere de forma satisfatória face aos requisitos especificados. / This work presents some constructive and operational aspects that should be take into account on the transformer design and specification. The design of the equipment is based on its technical specification. However, sometimes, it is observed that the technical specification does not contemplate some important points which could be crucial for the good transformer performance when in service. Generator step-up transformers are subject to some system disturbance where they are connected. The effect of these disturbances on the equipment could be minimize with a technical specification as complete as possible, on the sense of provide information regarding the network and connections between generator and power transformer. On the other hand, the manufacturer has the responsibility to interpret the technical requirements in order to design an equipment that operates satisfactory.
|
4 |
A semântica formal de MooZMin, Lin Tse January 1993 (has links)
Made available in DSpace on 2014-06-12T15:59:11Z (GMT). No. of bitstreams: 2
arquivo4936_1.pdf: 1288760 bytes, checksum: e9b38bddcefdbcf94c0812a3c4d81dc1 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 1993 / Este trabalho descreve uma semântica formal para MooZ, uma extensão µa linguagem Z
proposta pelo Grupo de Especificações Formais do DI/UFPE. Os conceitos fundamentais de
orientação a objetos foram incluídos em MooZ: abstração, encapsulamento, modularidade e
hierarquia.
A semântica formal é apresentada como uma extensão à semântica de variedades pro-
posta por J.M. Spivey para Z. A extensão traz como vantagens um maior entendimento
da facilidade de expressão de MooZ em relação à Z e a demonstração de que MooZ é uma
extensão conservativa de Z.
Após uma introdução informal à MooZ, os conceitos da teoria axiomática dos conjun-
tos de Zermelo-Fraenkel utilizados para descrever a semântica de MooZ são apresentados
e especificados em Z. O sistema de tipos de MooZ é descrito e o modelo de assinaturas,
estruturas e variedades de Spivey é expandido para comportar os conceitos de MooZ. As
funções semânticas que fornecem o significado de cada elemento de MooZ são definidas.
Por fim, são apresentadas a importância deste trabalho, as dificuldades encontradas no seu
desenvolvimento e as sugestões para a sua continuação
|
5 |
A framework for the specification and validation of Real Time Systems using Circus ActionSherif, Adnan January 2006 (has links)
Made available in DSpace on 2014-06-12T15:59:17Z (GMT). No. of bitstreams: 2
arquivo4988_1.pdf: 1332321 bytes, checksum: d7fe11f8136beac6845d4e2ab642bbda (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2006 / Circus é uma linguagem de especificação e programação que combina CSP, Z, e construtores do Cálculo do Refinamento. A semântica de Circus está baseada na Unifying Theories of Programming (UTP). Neste trabalho, estendemos um subconjunto de Circus com operadores de tempo. A nova linguagem é denominada de Circus Time Action. Propomos um modelo novo do tempo que estende o modelo da UTP, adicionando variáveis de observação para registrar a passagem de tempo. O novo modelo é usado para dar a semântica formal de Circus Time Action. Propriedades algébricas do modelo original de Circus são validadas no novo modelo; propriedades novas são exploradas e validadas dentro do contexto de Circus Time Action. A vantagem de utilizar o padrão de unificação proposto pela UTP é poder comparar e relacionar diferentes modelos. Definimos uma função de abstração, L, que faz o mapeamento das observações registradas no novo modelo (com tempo) para observações no modelo original (sem tempo); uma função inversa, R, é também definida. O objetivo é estabelecer uma ligação formal entre o modelo novo com tempo e o modelo original da UTP. A função L e sua função inversa R formam uma Galois Connection. Usando a função de abstração, nós introduzimos a definição de programas insensíveis ao tempo. A função de abstração permite a exploração de algumas propriedades não temporais de um programa. Apresentamos um exemplo simples para ilustrar o uso da função de abstração na validação de propriedades que não têm tempo associado. Entretanto, sistemas de tempo real têm requisitos temporais que necessitam ser validados. Neste sentido, propomos um framework para a validação de requisitos não temporais usando os dois modelos e a relação entre eles. A estrutura do framework é baseada em um processo de particionamento. Tendo como ponto de partida o programa e sua especificação escritos em Circus Time Action, aplicamos uma função sintática que gera uma forma normal do programa e sua especificação. A forma normal consiste de duas partes: a primeira é um programa sem operadores de tempo, mas com eventos que, por convenção, representam ações temporais; a segunda é uma coleção de temporizadores (timers) usados pelo programa. A composição paralela de ambas as partes é semanticamente equivalente ao programa original. Usando apenas o componente da forma normal que não envolve tempo explicitamente, mostramos que é possível raciocinar sobre propriedades de tempo no modelo não temporal; provamos formalmente a validade deste resultado. Para ilustrar o uso do framework, utilizamos um sistema de alarme simplificado como estudo de caso. Como a validação é reduzida ao modelo sem tempo, usamos a ferramenta de Model-Checking de CSP (FDR) para realizar as provas mecanicamente. Esta é uma outra contribuição importante deste trabalho
|
6 |
Produtividade na indústria da costrução : análise da influência da especificação de materiaisCunha, Vasco João Fernandes de Carvalho e January 2011 (has links)
No description available.
|
7 |
Manutenção de sistemas hidráulicos prediais : Manual de intervenção preventivaRamos, Hélder dos Reis January 2010 (has links)
No description available.
|
8 |
Specification of a space project management handbookBarbosa, Diana Maria dos Santos January 2012 (has links)
Estágio realizado na EFACEC - e orientado pelo Eng. Costa Pinto / Tese de mestrado integrado. Engenharia Electrotécnica e de Computadores. Faculdade de Engenharia. Universidade do Porto. 2012
|
9 |
Especificação formal,verificação e implementação de um protocolo de comunicação determinista, baseado em ethernetRegnier, Paul Denis Etienne 09 May 2008 (has links)
Submitted by Marcio Filho (marcio.kleber@ufba.br) on 2017-06-09T12:32:23Z
No. of bitstreams: 1
MestradoPaulRegnier.pdf: 1360286 bytes, checksum: 1fce559f768969919812613818682ff5 (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-06-12T15:27:57Z (GMT) No. of bitstreams: 1
MestradoPaulRegnier.pdf: 1360286 bytes, checksum: 1fce559f768969919812613818682ff5 (MD5) / Made available in DSpace on 2017-06-12T15:27:57Z (GMT). No. of bitstreams: 1
MestradoPaulRegnier.pdf: 1360286 bytes, checksum: 1fce559f768969919812613818682ff5 (MD5) / Este trabalho apresenta um protocolo que torna o uso compartilhado de Ethernet eficiente para dar suporte aos sistemas de tempo real modernos. O protocolo foi especificado formalmente e sua correção foi atestada automaticamente através de um verificador de modelo. Em seguida,
um protótipo foi realizado numa plataforma operacional de tempo real. Os resultados
experimentais confirmaram a capacidade do protocolo em atender os objetivos definidos na sua
proposta.
As aplicações que podem se beneficiar deste protocolo são principalmente aquelas compostas
de dispositivos heterogêneos e distribuídos que têm restrições temporais de natureza críticas
e não-críticas. Utilizando o protocolo proposto, tais sistemas podem utilizar o mesmo barramento
Ethernet de forma eficiente e previsível. A utilização do barramento é otimizada através
da alocação apropriada da banda disponível para os dois tipos de comunicação. Além disso, o protocolo, compatível com os dispositivos Ethernet comuns, define um controle descentralizado do acesso ao meio que garante flexibilidade e confiabilidade à comunicação.
|
10 |
Hiperbolicidadade e Propriedade de EspecificaçãoMorro, Marcus Vinícius 25 February 2013 (has links)
Submitted by Marcio Filho (marcio.kleber@ufba.br) on 2016-06-07T13:47:42Z
No. of bitstreams: 1
dissert_marcus.pdf: 773867 bytes, checksum: a2c541e32cded5b3c0d8e4eab71e0406 (MD5) / Approved for entry into archive by Uillis de Assis Santos (uillis.assis@ufba.br) on 2016-06-07T18:45:24Z (GMT) No. of bitstreams: 1
dissert_marcus.pdf: 773867 bytes, checksum: a2c541e32cded5b3c0d8e4eab71e0406 (MD5) / Made available in DSpace on 2016-06-07T18:45:24Z (GMT). No. of bitstreams: 1
dissert_marcus.pdf: 773867 bytes, checksum: a2c541e32cded5b3c0d8e4eab71e0406 (MD5) / Seja f um difeomorfismo de uma variedade fechada C∞. Neste trabalho,
apresentamos a noção de propriedade de especificação C1-estável para um
conjunto f-invariante Λ de M, e apresentamos a prova de que f|Λsatisfaz a
propriedade de especificação C1-estável se e somente se Λ é um conjunto elementar hiperbólico.
|
Page generated in 0.0722 seconds