Diseño y construcción de programas mediante CSP

Abstract

En este artículo presentamos, a través de un caso de estudio, el desarrollo de programas paralelos mediante métodos formales. El caso de estudio es el núcleo básico de un sistema operativo multitarea, y el método formal utilizado es la teoría de procesos secuenciales comunicantes, CSP. CSP es una teoría de programación que permite modelar sistemas mediante procesos comunicantes. Los procesos se modelan mediante un conjunto de eventos observables del sistema a implantar. CSP dispone de un lenguaje de especificación que permite describir el comportamiento de los procesos a través de sus eventos observables. La especificación inicial de un sistema debe ser lo suficientemente abstracta para indicar lo que el sistema debe hacer, sin dar detalles de cómo lo hace. Para dar tales detalles, una especificación debe refinarse de manera paulatina; esto se hace a través de pasos de refinamiento. En cada paso de refinamiento se debe probar que el refinamiento satisface los criterios de la especificación original; para dar tal garantía, CSP dispone de un conjunto de leyes algebraicas. El diseño y construcción del núcleo básico de un sistema operativo inicia con la especificación del entrelazamiento de acciones que modela nuestra intuición del paralelismo de un monitor multitareas. Esta especificación es refinada para itroducir los mecanismos necesarios para implantar la conmutación entre tareas del monitor. Se da la prueba formal de ciertos refinamientos y en otros, donde la complejidad aumenta, utilizamos FDR, un sistema que de manera automática, verifica la corrección de los refinamientos.