Publicação
Using CafeOBJ to implement a reduction strategy in the context of hardware/software partitioningUsing CafeOBJ to implement a reduction strategy in the context of hardware/software partitioningUsing CafeOBJ to implement a reduction strategy in the context of hardware/software partitioning
| Resumo: | 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 de- scription 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. |
|---|---|
| Autores principais: | Silva, André Luís Meneses |
| Outros Autores: | Menezes, Manoel Messias; Silva, Leila |
| Assunto: | Verificação de particionamento Sistemas de reescrita Hardware Software |
| Ano: | 2014 |
| País: | Brasil |
| Tipo de documento: | artigo |
| Tipo de acesso: | acesso aberto |
| Instituição associada: | IBICT |
| Idioma: | português |
| Origem: | Oasisbr |
| Resumo: | 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 de- scription 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. |
|---|
Atividades financiadas
Não foram encontrados projetos financiados.