Refinamento Formal De Sistemas
Mostrando 1-12 de 16 artigos, teses e dissertações.
-
1. Estendendo CRefine para o suporte de táticas de refinamento
A utilização de aplicações de software cada vez mais complexas está exigindo um maior investimento no desenvolvimento de sistemas, garantindo uma melhor qualidade das aplicações. Diante desse contexto, novas técnicas estão sendo utilizadas na área de Engenharia de Software, tornado o processo de desenvolvimento mais eficaz. Destacam- se, co
IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia. Publicado em: 07/10/2011
-
2. Uma biblioteca de padrões de especificação em Event-B para mecanismos de troca de mensagens em sistema distribuídos
O desenvolvimento de sistemas distribuídos e protocolos de comunicação é uma tarefa complexa e o uso de técnicas de especificação e verificação formal torna-se necessário para garantir a corretude de tais sistemas. Enquanto técnicas de model-checking passam pelo problema da explosão do espaço de estados, o uso de provadores de teoremas represent
IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia. Publicado em: 19/03/2010
-
3. Geração de casos de teste a partir de especificações B
Com o crescente aumento da complexidade dos sistemas de software, há também um aumento na preocupação com suas falhas. Essas falhas podem causar prejuízos financeiros e até prejuízos de vida. Sendo assim, propomos neste trabalho a minimização de falhas através de testes em softwares especificados formalmente. A conjunção de testes e especificaç�
Publicado em: 2010
-
4. Abstraction of infinite and communicating CSPZ processes
Esta tese trata de um problema muito comum em verificaÃÃo formal: explosÃo de estados. O problema desabilita a verificaÃÃo automÃtica de propriedades atravÃs da verificaÃÃo de modelos. Isto à superado pelo uso de abstraÃÃo de dados, em que o espaÃo de estados de umsistema à reduzido usandoumprincÃpio simples: descartando detalhes de tal forma
Publicado em: 2009
-
5. Um método de refinamento para desenvolvimento de software embarcado: uma abordagem baseada em UML-RT e especificações formais. / A refinement method for embedded software development: a based UML-RT and formal specification approach.
Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal atr
Publicado em: 2007
-
6. Mapeamento da linguagem Nautilus para Java
Este trabalho apresenta um mapeamento centrado nas construções não usuais da linguagem Nautilus, para a linguagem convencional, no caso Java, mantendo propriedades com atomicidade que são requisitos da semântica formal da linguagem. Nautilus é originalmente uma linguagem de especificação baseada em objetos, textual que suporta objetos concorrentes e
Publicado em: 2007
-
7. BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B
A tecnologia Java Card permite o desenvolvimento e execução de pequenas aplicações embutidas em smart cards. Uma aplicação Java Card é composta por um cliente, externo ao cartão, e por uma aplicação contida no cartão que implementa os serviços disponíveis ao cliente por meio de uma Application Programming Interface (API). Usualmente, essas aplic
Publicado em: 2007
-
8. Ontology-based metadata for e-learning content
Atualmente a popularidade da Web incentiva o desenvolvimento de sistemas hipermídia dedicados ao ensino a distância. Não obstante a maior parte destes sistemas usa os mesmos recursos do ensino tradicional, apresentado o conteúdo como páginas HTML estáticas, não fazendo uso das novas tecnologias que a Web oferece. Um desafío atual é desenvolver siste
Publicado em: 2007
-
9. A refinement theory for alloy / A refinement theory for alloy
Refatoramentos sÃo geralmente propostos de maneira ad hoc, porque à difÃcil provar formalmente que eles preservam comportamento. Na prÃtica, desenvolvedores, mesmo utilizando ferramentas de refatoramento, tÃm que usar compilaÃÃo e testes para garantir que os refatoramentos sÃo corretos. Esse cenÃrio nÃo à desejado principalmente no desenvolvimento
Publicado em: 2007
-
10. GeraÃÃo de especificaÃÃo formal de sistemas a partir de documento de requisitos
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 lingu
Publicado em: 2006
-
11. Gerenciamento baseado em modelos da configuração de sistemas de segurança em ambientes de redes complexos / Model-based configuration management of security systems in complex network environments
Os mecanismos de segurança empregados em ambientes de redes atuais têm complexidade crescente e o gerenciamento de suas configurações adquire um papel fundamental para proteção desses ambientes. Particularmente em redes de computadores de larga escala, os administradores de segurança se vêem confrontados com o desafio de projetar, implementar, manter
Publicado em: 2006
-
12. VerificaÃÃo de modelos para programas em um subconjunto de JCSP
A veriÂcaÂc~ao de modelos formais gerados a partir de programas concorrentes tem sido bem aceita na indÃstria e na academia durante a fase de testes. A busca por qualidade de software tem motivado este uso, principalmente pelo fato de que testar programas concorrentes nÃo à uma tarefa trivial e à suscetÃvel a erros. Os modelos sÃo descritos atravÃs
Publicado em: 2006