Implementando uma estratégia de redução para o contexto de Sistemas Embarcados usando CafeOBJ

Abstract

The focus of this work is hardware/software partitioning verification. The approach uses occam as specification and reasoning language. The partitioned system is derived from the original description of the system by applying transformation rules, all of them proved from the basic laws of occam. The aim of this work is to show how the rewriting system CafeOBJ can be used to automatically prove the partitioning rules, as well as to implement the reduction strategy that guides the application of these rules. In this way, rewriting systems can be regarded as supporting tools for the construction of partitioning environments, whose emphasis is correctness. _________________________________________________________________________________________ RESUMO: Este artigo insere-se no âmbito da verificação formal do particionamento de sistemas em componentes de hardware e software. A abordagem adotada usa occam como linguagem de especificação e raciocínio. A descrição do sistema particionado é derivada da descrição original do sistema, mediante o emprego de regras de transformação, estas provadas usando-se as leis básicas de occam. O objetivo principal deste trabalho é explorar o uso do sistema de reescrita CafeOBJ na mecanização das provas das regras para o particionamento, bem como da estratégia de redução que gera a aplicação destas regras. Desta forma, sistemas de reescrita podem ser considerados ferramentas de suporte para a construção de um ambiente para o particionamento, cuja ênfase é o rigor formal.