Explorando o Uso de Sistemas de Reescrita como Ferramenta de Suporte no Contexto do Particionamento de Hardware e Software

• Manoel Messias Menezes UFS
• André Luis Silva UFS
• Leila Silva UFS

Resumo

Este artigo insere-se no âmbito da verificação formal do particionamento de sistemas em componentes de hardware e software. A abordagem adotada deriva o sistema particionado a partir da descrição original, mediante o emprego de regras de transformação. O objetivo principal deste trabalho é explorar o uso de sistemas de reescrita na mecanização das provas das regras para o particionamento, bem como da estratégia de redução que guia 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.

Referências

Clavel, M., Durán, F., Eker, S., Lincoln, P., Marti-Oliet, N., Meseguer, J. e Quesada, J. F. (1999) Maude: Specification and Programing in Rewriting Logic. Computer Science Laboratory-SRI International.

Goguen, Joseph. Fun with BOBJ. Disponível on-line: [link]. Último acesso 11/03/2003.

Goguen, Joseph A., Winkler, T., Meseguer, J., Kokichi, F. e Jean P, J (1992). Introducing OBJ*, Relatório Técnico. SRI-CSL-92-03, SRI International, Computer Science Laboratory.

Hsieh, H., A. Sangiovanni-Vicentelli, F. Ballarin e L. Lavagno. (1999), Synchronous Equivalence for Embedded Systems: A Tool for Design Exploration, em Proceedings of the International Conference on Computer-Aided Design, pp. 505-509.

Hughes, R. B. e Musgrave, G. (1996) The Lambda Approach to System Verification. Em Hardware/Software Co-design, Kluwer Academic Publisher, 427-451.

Kern, C e M. Greenstreet. Formal Verification in Hardware Design: A Survey (1999), ACM Transactions in Design Automation of Eletronic Systems, 4(2):123-193.

Jones, G. e Goldsmith, M. (1998) Programing in occam 2. Prentice-Hall.

Lira, B, Cavalcanti, A. e Sampaio, A. (2002) Automation of a Normal Form Reduction Strategy for Object-Oriented Programming. Proc. of 5th Workshop on Formal Methods, 193-208.

Menezes, M., Silva, A. e Silva, L. (2003) Verificação Formal da Etapa do Particionamento em Co-design Usando o Sistema de Reescrita BOBJ. Anais do XXX Seminário Integrado de Hardware e Software, pp. 195-210.

Nakagawa.A., Sawada T. e Futatsugi, K (1999) CafeOBJ user’s manual ver 1.4.2. Disponível on-line: [link]. Último acesso 01/07/2003.

Niemann, R. e Marwedel, P. (1997) An Algorithm for Hardware/Software Partitioning Using Mixed Integer Linear Programming. Design Automation of Embedded Systems, 2(2):165-193.

Roscoe, A. W. e Hoare, C.A.R. (1988) The Laws of occam programming. Theoretical Computer Science, 60:177-229.

Saha, D., Mitra, R. S. e Basu, A. (1997) Hardware/Software Partitioning Using Genetic Algorithm. Proc. of 10th International Conference on VLSI Design, India, 155-160.

Sampaio, A. (1997) An Algebraic Approach to Computer Design. Volume 4 of Algebraic Methodology and Software Technology (AMAST) Series in Computing, World Scientifc.

Silva, A., Menezes, M. e Silva, L. (2003) Using CafeOBJ to implement a Reduction Strategy in the Context of Hardware/Software Partitioning. Proc. of 6th Workshop on Formal Methods, pp 43-58. Também em Electronic Notes in Theoretical Computer Science 95C pp. 63-82.

Silva, A e Menezes, M. (2004) Explorando Sistemas de Reescrita no Contexto de Co-design, Monografia de final de curso, Universidade Federal Sergipe.

Silva, L. (2000) An Algebraic Approach to Hardware/Software Partitioning. Tese de Doutorado. Universidade Federal de Pernambuco, Recife, Pernambuco.

Silva L., Sampaio A. e Barros E. (2004) A Constructive Approach to Hardware/Software Partitioning. Journal of Formal Methods in Systems Design, 24:45-90.