Spelling suggestions: "subject:"metodos formais""
1 |
Uma exposição formal para a composição de frameworksMiranda Mesquita Neto, Walter January 2004 (has links)
Made available in DSpace on 2014-06-12T15:59:33Z (GMT). No. of bitstreams: 2
arquivo5175_1.pdf: 1994160 bytes, checksum: 29002a3ad03ec142019fe6f3747721fb (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2004 / O desenvolvimento de aplica¸c oes baseado em frameworks tem sido apontado como
o pr´oximo passo em dire¸c ao a um maior reuso de software. O reuso atrav´es da
composi¸c ao de dois frameworks, e n ao apenas atrav´es de extens oes de classes de
um ´unico framework, tornou-se uma necessidade gerada pelo aumento da complexidade
de desenvolvimento de sistemas computacionais. Neste sentido, tornam-se
necess´arias novas t´ecnicas de documenta¸c ao ou especifica¸c ao de frameworks que
eliminem imprecis oes e ambig¨uidades nas descri¸c oes dos seus comportamentos.
Este trabalho apresenta uma estrat´egia de composi¸c ao de frameworks que utiliza
linguagens de especifica¸c ao formal para descrever seus comportamentos e estruturas
de dados. As linguagens utilizadas s ao CSP, Z e CSP-Z. Por tratar da
composi¸c ao no n´ıvel das especifica¸c oes formais, a estrat´egia consegue abstrair detalhes
de implementa¸c ao e eliminar restri¸c oes ligadas a estes detalhes. Al´em disso,
a abordagem formal permite a verifica¸c ao, atrav´es do verificador de modelos de
CSP, FDR, da manuten¸c ao das propriedades dos frameworks originais.
O objetivo principal da estrat´egia ´e a composi¸c ao de fluxos de controle, que ´e
um dos problemas mais comuns da composi¸c ao de frameworks. N´os apresentamos
as causas e poss´ıveis solu¸c oes deste e dos demais problemas da composi¸c ao de
frameworks. Por fim, mostramos que a estrat´egia aborda todos os problemas
listados em menor ou maior grau.
A estrat´egia pretende realizar a comunica¸c ao entre os frameworks atrav´es de um
casamento entre os eventos e tipos de dados correspondentes dos dois frameworks.
A composi¸c ao ´e realizada atrav´es de um terceiro componente, o componente de
sincroniza¸c ao e comunica¸c ao (CSC). A ado¸c ao deste componente possibilita maior
flexibilidade `a composi¸c ao e, entre outros benef´ıcios, permite que os frameworks
se comuniquem de forma an onima e elimina efeitos colaterais nos seus comportamentos.
A estrat´egia tem todos os seus pontos especificados num n´ıvel de detalhe que
facilitar´a uma futura mecaniza¸c ao. Neste sentido, s ao apresentados modelos para
a especifica¸c ao do CSC e uma abordagem construtiva para a sua gera¸c ao
|
2 |
Estimativa de consumo de energia de c¶odigo ANSI-C para sis- temas embarcados: uma abordagem baseada em simula»c~ao estoc¶asticaRoncalli Novaes Pires Ribeiro, Angelo January 2007 (has links)
Made available in DSpace on 2014-06-12T16:00:15Z (GMT). No. of bitstreams: 2
arquivo6285_1.pdf: 1527923 bytes, checksum: 78d4cb768e2160db1bd4ea015fdefa03 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2007 / Sistema Embarcado ¶e um sistema computacional projetado para uma fun»c~ao dedicada.
Geralmente, este sistema executa uma tarefa espec¶³¯ca dentre um conjunto maior de
tarefas, e possui particularidades tanto de hardware quanto de software.
Os Sistemas Embarcados est~ao presentes no cotidiano sob diferentes formas e com
diferentes objetivos. Geralmente possuem uma s¶erie de restri»c~oes, tais como: dimens~oes
das mem¶orias, fonte de energia, baixa velocidade de processamento, dentre outras.
Este trabalho apresenta o desenvolvimento de um modelo em Redes de Petri de desem-
penho e energias para c¶odigos ANSI-C, considerando um processador de uma plataforma
embarcada espec¶³¯ca, com o objetivo de estimar o consumo de energia.
A linguagem ANSI-C, como c¶odigo de Sistemas Embarcados, foi escolhida por ser uma
das mais utilizadas no desenvolvimento destes sistemas. Redes de Petri Temporizadas
permitem a modelagem e especi¯ca»c~ao de sistemas paralelos e distribu¶³dos e, ao mesmo
tempo, prov^eem o formalismo matem¶atico necess¶ario para uma avalia»c~ao de desempenho.
Neste trabalho, o modelo Redes de Petri Temporizada ¶e anotado com informa»c~ao de
consumo de energia, o que originou a Power Petri Net.
Este trabalho contribui tamb¶em com a implementa»c~ao de um simulador estoc¶astico
para avalia»c~ao de desempenho e de um ambiente computacional no qual s~ao realizadas
as estimativas. Esse ambiente ¶e formado pelo tradutor de c¶odigo ANSI-C para Redes de
Petri no formato PNML [1], padr~ao XML para descri»c~ao de Redes de Petri, simulador
estoc¶astico e extens~ao do ambiente EzPetri [2]. Como o modelo apresentado, b¶asico, pode
ser estendido em outros trabalhos ¶e caracterizada a forma»c~ao de um framework.
Para valida»c~ao do m¶etodo proposto, foi utilizado um c¶odigo de avalia»c~ao, benchmark,
PowerStone [3] desenvolvido para explorar o sistema sob diferentes aspectos de consumo
de energia
|
Page generated in 0.0655 seconds