PDF de programación - Tesis: Manuel Aguilar - Especificacion y diseño del nucleo basico de un sistema operativo mediante CSP

1'/ '19'(- t:'l
1E_.J'./ ·; 11:,

cW.rlll I~ IIIYE '?TIUCit. Y ~~

UIT~i'!lll ;> AV A,. l • US IH

!. P . N .

li§ L_ ; OT EC A

•
! •··~E: NIERIA EL ECTRIO

CENTRO DE INVESTIGACION Y DE ESTUDIOS

A V ANZADOS DEL I.P.N.

Departamento de Ingenieria Electrica

Secci6n Computaci6n

Tesis de Maestria:

CIN ·ESTAV

p N

ADOUI SICION
DE Li8~0S

" Esp ecificacion y disefio del nucleo basico de un s istema op erativo

mediante CSP "

Que para obtener el grado de Maestro en Ciencias en Ia especialidad de

Ingenierfa Electrica con Opci6n Computaci6n

Presenta:

Manuel Aguilar Cornejo' LY n t 1£ Illn:snuc11~; v . ,

ESTUDIIS AVA i•7.•. 89S H l

Dirigida por:

!. F". N .

I 1!1 L

•
,a..
lAJ C.: t:N IERiA ELE CTRIC-'

I C.) T £ C

Dr. Hector Rufz Barradas2

Mexico, D. F., Mayo de 1997

1 Becario de CONACYT y Pro f. asoc iad o de tiempo completo de Ia UAM lztapa lapa
2 Prof. in vestigador de tiem po completo de l area de S istemas Digitales del Depto. de lng . E lect r6 nica de Ia UAM
Azcapotzalco

iL.aiJa.,,i__'iL_G __ _
ADGUIS. ; ~_:-.l::L'l. 'i:L
~'•CHA ':J .• =Sf'ffl.::.":t..L
"IIOCED. t.<:;.S.J.J . .::JS.11.:._

•.............

.. --

CENTRO DE INVESTIGACION Y DE ESTUDIOS

A V ANZADOS DEL I.P.N.

Departamento de Ingenierfa Eh!ctrica

Secci6n Computaci6n

Tesis de Maestrfa:

" Esp ecificaci6n y diseiio del m~cleo basico de un sistema operativo

mediante CSP "

Que para obtener el grado de Maestro en Ciencias en Ia especialidad de

Ingenierfa Electrica con Opci6n Computaci6n

Presenta:

Manuel Aguilar Cornejo 1

Dirigida por:

Dr. Hector Rufz Barradas2

Mexico, D. F., Mayo de 1997

1 Becari o de CONACYT y Prof asoc iado de ti empo comp leto de Ia UAM lztapa la pa
' Prof in vesti gador de tiempo compl eto de l area de S istemas Dig ita les de l Depto. de In g. Electro nica de Ia UAM
Azcapotza lco

A mis padres:

Que gracias a sus cuidados, consejos y apoyo dieron sentido a mi
vida, convirtiendose asi, en mis primeros maestros.

A mis hermanos:

Que gracias a su compama y apoyo han contribuido en la
felicidad y alegria que han acompafiado mi vida, siendo asi mis
primeros compafieros.

Agradecimientos

Quiero agradecer a un sinnumero de personas, familiares e instituciones por el apoyo
y confianza que me han brindado, me disculpo de antemano si es que omito a alguna
persona o a varias. Agradezco sinceramente a:

Mi familia. Gracias por el apoyo economico, moral, y por Ia confianza que me han
brindado a lo largo de mi vida

CONACYT. Gracias por el apoyo economico que nos brinda a muchos estudiantes de
posgrado

UAM Iztapalapa. Gracias por haberrne liberado de muchas de mis labores academicas
para realizar mis estudios de maestria. Gracias por haberme brindado el equipo necesario
para concluir mi
tesis y gracias a mis alumnos por su comprension cuando
esponidicamente falte a clases.

Mi asesor de Tesis. Gracias a ti Hector por haber aceptado dirigir mi tesis, gracias por
tu paciencia y apoyo, gracias por compartir un poco de tus conocimientos con nosotros,
tus alumnos, gracias por ser una excelente persona y un excelente investigador.

A mis sinodales. Gracias a Ia Ora. Elizabeth Perez C., al Dr. Ju Shiguang y nuevamente
al Dr. Hector Ruiz B. por aceptar formar parte del jurado asumiendo lo que esto implica
Agradezco a cada uno de ellos, a Hector por haber dirigido mi tesis; a Ia Ora. Elizabeth
por su paciencia en Ia revision de mi tesis, por su apoyo, por sus consejos y por ser una
excelente persona; y al Dr. Ju por haber aceptado ser parte del jurado, por sus consejos
y por ser un gran amigo

A mis compaiieros. Agradezco a todos los compaiieros que tuve en Ia seccion de
computacion por haber hecho de mi estadia en Ia maestria, una de las etapas mas felices y
alegres de mi vida, conservare en Ia memoria y en medios de almacenamiento los
momentos mas felices que pasamos juntos. En particular agradezco a: Alfredo Yanez,
Alicia, Carlos Campos, Carlos Hdz., Cesar Vargas, David Perez, Eduardo Camargo,
Efren Lopez, Enrique Sanchez, Estela Canchola, Francisco Mtz., Francisco Zaragoza,
Gonzalo Aviles, Heberto Ferreira, Ignacio Vega, Jesus Naro, Jose Mitre, Manuel Diaz,
Marco, Marcos Marvan, Marco Rueda, Martha Cordero, Nuri Custodio, Raul Hdz.,
Ricardo Diaz, Samuel Cortes y Tanit Cruz. Gracias por haber sido excelentes
compaiieros. Gracias por su amistad

A mis amigos. Les doy las gracias por su amistad y apoyo a Javier Delgado A ,
Emiliano Zapata M ., Emelio Campos F. , Anabel Diaz, Sofia Reza, Flor Cordova y muy
en particular a Sandra Diaz S. por las palabras de aliento, y por ser una excelente amiga.
Agradezco tambien al resto de mis amigos que por fines de espacio no menciono aqui

Sinceramente

Manuel Aguilar C.

Resumen

En este trabajo presentamos, a traves de un caso de estudio, el desarrollo de sistemas
mediante metodos formales . El caso de estudio es el nucleo basico de un sistema
operativo multitareas y el metodo formal utilizado es Ia teoria de Procesos Secuenciales
Comunicantes (CSP)

Comenzamos este trabajo dando una muy breve explicaci6n de lo que son los
metodos formales en general, para despues presentar de manera particular el metodo
formal de CSP, asi como un demostrador automatico de refinarnientos CSP, denominado
FOR (Refinarnientos Falla-Oivergencia). Posteriormente desarrollamos el sistema
seleccionado mediante CSP

Comenzamos el desarrollo de nuestro caso de estudio con Ia especificaci6n inicial
del nucleo basico del sistema operativo, en donde solo expresamos lo que queremos
realizar sin dar detalles de implantaci6n. Los detalles de implantaci6n los damos de
manera gradual en lo se denorninan pasos de refinamiento, en cada uno de ellos
refinamos una propiedad del sistema. Cada refinarniento debe conservar las propiedades
esenciales de Ia especificaci6n inicial, para asegurarnos de ello realizamos pruebas
formales, por un lado usando el algebra de procesos CSP y por otro lado usando FOR.
Una vez que obtuvimos un refinarniento con los suficientes detalles de implantaci6n
derivamos un programa en pseudoc6digo.

Terrninamos Ia exposici6n de este trabajo con nuestras conclusiones y un par de
apendices. En el primer apendice mostramos las !eyes CSP utilizadas en el texto, en el
segundo apendice damos un listado de Ia especificaci6n inicial y de los refinarnientos del
nucleo basico del sistemas operativo.

Palabras clave:

Metodo formales, CSP (Procesos Secuenciales Comunicantes), FOR (Refinarnientos
Falla-Oivergencia), pasos de refinarniento, lenguaje de especificaci6n formal , sistema de
inferencia, proceso, evento, paralelismo, concurrencia, deterrninismo, no determinismo,
sistemas criticos, correcci6n.

Abstract

In this thesis is presented, trough a case study, the development of systems by the
use of formal methods. The case study is the basic kernel of a multitasking operating
system, and the formal method used is the Communications Sequential Processes (CSP) .

The thesis begins by giving a brief general explanation of formal methods, and
then describes the CSP formal method and an automatic refinements proof for CSP,
called FDR (Failures-Divergence Refinements). Lately we present the development of
the selected system in CSP.

The development of the case study commences with the initial specification of the
basic operating system kernel, where we just express what we what to do, without
implementation details. Such implementation details are given in a gradual form in the
named "refinement steps", in each of which, we refine a property of the system. All
refinements have to conserve the essential properties of the initial specification. To
ensure that such properties are conserved, we give formal proofs, using the algebra of
processes CSP, and also FDR. Once a refinement with enough implementation details is
obtained, we derive a program in pseudocode.

We finish the exposition of this work with our own conclusions and a couple of
appendixes. In the first appendix we show the CSP laws used in the text, in the second
one we give a listening about the initial formal specification and the refinements of the
basic operating systems kernel.

key words:

Formal methods, CSP
Divergence Refinement), refinement steps, formal specification language, inference
systems, processes, event, parallelism, concurrence, determinism, non determinism,
critical systems, correctness.

(Communications Sequential Processes), FDR (Failures

Capitulo 1. Introduccion

. ... .... . .... . .. . . . .... .. . . . . . . .. . . .. .. . . . . .

1. 1 Introduccion
1.2 Metodos formales .
1.3 Ellenguaje de especificacion formal
1.4 El sistema de Prueba ................... . ..... . .
I . 5 Desarrollo de sistemas usando metodos formales
I .6 Estructura de Ia tesis .

4
6
7

9
II

Capitulo 2. C.S.P. (Procesos Secuenciales Comunicantes) . . . . . . . . . . . . . . . . . . 13

2.I Procesos

. . . ......... .

.... . . . . . . .. . .

2.I .I Prefijo
2.1.2 Recursion
2.1.3 Eleccion
2.I.4 Recursion mutua
2. I .S Trazas

2.1.S .I Operacion sobre trazas

2.1.6 Trazas de un proceso

2.1.6.I Leyes sobre trazas de un proceso

2.2 Concurrencia

2.2. I Tr