masterThesis
Especificação do micronúcleo FreeRTOS utilizando o método B
Fecha
2011-08-16Registro en:
GALVÃO, Stephenson de Sousa Lima. Especificação do micronúcleo FreeRTOS
utilizando o método B. 2011. 117 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2011.
Autor
Galvão, Stephenson de Sousa Lima
Resumen
This paper presents a contribution to the international Verified Software Repository
effort through the formal specification of the microkernel FreeRTOS real-time system.
Such specification was made in abstract level making use of the B method . For thus,
properties of the microkernel were chosen and selected as specification requisites, which
was constructed centered at the functionalities responsible for the utilization of these properties.
This properties weres setting as specification requirements. The specification was
constructed modeling the function of microkernel that implement this properties. This
work intended to encourage the formal verification of FreeRTOS and also contribute to
the formal creation of a microkernel real-time systems, based in FreeRTOS. Furthermore,
this model brings a formal documentation point view of the microkernel, demonstrating
features and how this internal states is changing. Finally, this work could be an example
of specification of the actual system by the B method.