Abstract Specification of an Operating System Kernel and Its Formalization in the Z Language
Abstract
One of the mini challenges in software verification related to the Grand Challenge defined by Tony Hoare concerns the formal specification and verification of an operating system kernel. This paper proposes a simple and correct (yet preliminary) specification of an OS kernel in Z, which simplifies the understanding and verification of operating system components.References
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.
Published
2010-07-20
How to Cite
BARRETO, Luciano; ANDRADE, Aline; DURAN, Adolfo; LIMA, Caíque; LIMA, Ademilson.
Abstract Specification of an Operating System Kernel and Its Formalization in the Z Language. In: WORKSHOP ON OPERATING SYSTEMS (WSO), 7. , 2010, Belo Horizonte/MG.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2010
.
p. 2011-2021.
