Especificação Abstrata do Núcleo de um Sistema Operacional e sua formalização na linguagem Z
Resumo
A especificação formal e verificação do núcleo de um sistema operacional constitui um dos mini desafios propostos pela comunidade de métodos formais no contexto dos Grandes Desafios em verificação de software (Grand Challenges) proposto por Tony Hoare. Este artigo apresenta uma proposta de kernel simples e correto (ainda que preliminar) especificada em Z, que simplifica a compreensão e verificação de componentes do sistema operacional.Referências
Bevier, W. R. (1989). Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382–1396.
Craig, I. D. (2007). Formal Refinement for Operating Systems Kernels. Springer.
Gallardo, M. D. M., Merino, P., and Sanán, D. (2009). Model checking dynamic memory allocation in operating systems. Automated Reasoning, 42(2-4):229–264.
Hoare, C. A. R. (2003). The verifying compiler software grand challenge for computer research. Journal of ACM, 50(1):63–69.
Klein, G., Derrin, P., and Elphinstone, K. (2009a). Experience report: sel4: formally verifying a high-performance microkernel. In Proceedings of the 14th ACM SIGPLAN international Conference on Functional Programming (ICFP), pages 91–96, New York, NY, USA. ACM.
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and Winwood, S. (2009b). sel4: formal verification of an os kernel. In Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP), pages 207–220, New York, NY, USA. ACM.
Liedtke, J. (1995). On micro-kernel construction. In Proceedings of the 15th Symposium on Operating Systems Principles (SOSP), pages 237–250, New York, NY, USA. ACM.
Saaltink, M. (1997). The z/eves system. In Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation (ZUM), pages 72–85, London, UK. Springer-Verlag.
Walker, B. J., Kemmerer, R. A., and Popek, G. J. (1980). Specification and verification of the ucla unix security kernel. Commun. ACM, 23(2):118–131.
Woodcock, J. and Davies, J. (1996). Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
Yang, J., Twohey, P., Engler, D., and Musuvathi, M. (2006). Using model checking to find serious file system errors. ACM Transactions on Computer Systems, 24(4):393–423.
Craig, I. D. (2007). Formal Refinement for Operating Systems Kernels. Springer.
Gallardo, M. D. M., Merino, P., and Sanán, D. (2009). Model checking dynamic memory allocation in operating systems. Automated Reasoning, 42(2-4):229–264.
Hoare, C. A. R. (2003). The verifying compiler software grand challenge for computer research. Journal of ACM, 50(1):63–69.
Klein, G., Derrin, P., and Elphinstone, K. (2009a). Experience report: sel4: formally verifying a high-performance microkernel. In Proceedings of the 14th ACM SIGPLAN international Conference on Functional Programming (ICFP), pages 91–96, New York, NY, USA. ACM.
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and Winwood, S. (2009b). sel4: formal verification of an os kernel. In Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP), pages 207–220, New York, NY, USA. ACM.
Liedtke, J. (1995). On micro-kernel construction. In Proceedings of the 15th Symposium on Operating Systems Principles (SOSP), pages 237–250, New York, NY, USA. ACM.
Saaltink, M. (1997). The z/eves system. In Proceedings of the 10th International Conference of Z Users on The Z Formal Specification Notation (ZUM), pages 72–85, London, UK. Springer-Verlag.
Walker, B. J., Kemmerer, R. A., and Popek, G. J. (1980). Specification and verification of the ucla unix security kernel. Commun. ACM, 23(2):118–131.
Woodcock, J. and Davies, J. (1996). Using Z: specification, refinement, and proof. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
Yang, J., Twohey, P., Engler, D., and Musuvathi, M. (2006). Using model checking to find serious file system errors. ACM Transactions on Computer Systems, 24(4):393–423.
Publicado
20/07/2010
Como Citar
BARRETO, Luciano; ANDRADE, Aline; DURAN, Adolfo; LIMA, Caíque; LIMA, Ademilson.
Especificação Abstrata do Núcleo de um Sistema Operacional e sua formalização na linguagem Z. In: WORKSHOP DE SISTEMAS OPERACIONAIS (WSO), 7. , 2010, Belo Horizonte/MG.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2010
.
p. 2011-2021.
