Download Introducción al Modelado de Sistemas Proyecto 1: hospital

Introducción al Modelado de Sistemas
Proyecto 1: hospital
profesor: Camilo Rueda
27 de septiembre de 2012
En este proyecto debe modelar un sistema de múltiples agentes para un hospital. El
sistema consiste de dos clases de agentes, pacientes y personal médico (doctores). La condición de cada paciente se monitorea por el correspondiente equipos médico (un agente que
representa al paciente). Los agentes doctores corren en asistentes personales (por ejemplo, iPad’s). El hospital tiene conexión inalámbrica para estos “doctores”. Cada doctor
está asociado con un agente.
El equipo médico actualiza continuamente el registro del paciente. En caso de emergencia, el agente paciente genera una llamada de emergencia que se comunica al doctor que
trata al paciente. Una condición de seguridad importante es que “todas las emergencias
deben tratarse con prontitud por los doctores”. Como este requisito es difcil de cumplir
siempre, el sistema garantiza al menos que cada llamada de emergencia eventualmente ser
tratada por algún doctor. Además, diferentes doctores pueden asociarse al mismo paciente, debido a rotaciones del personal médico. Se debe asegurar entonces que al final de la
jornada de un doctor, todos sus pacientes se transfieran a otro doctor.
Otro requisito importante es que un doctor siempre accede al registro más reciente de
datos del paciente y que este siempre esta al dı́a. Asumimos que el registro de cada paciente
se guarda en el dispositivo del médico que lo atiende. Cada tratamiento o droga prescrita se
introduce en los datos del paciente por el doctor, mediante su iPad (o dispositivo similar).
Todas las modificaciones se sincronizan con los datos que guarda el equipo del paciente.
Cuando el doctor termina de examinar al paciente o de prescribir una droga, la conexión
con los datos del paciente se pierden. Esto nos asegura que solamente el doctor que esté en
proximidad con el paciente pueda modificar los datos del paciente.
A continuación se presenta un modelo abstracto y un refinamiento de este sistema.
Usted debe construir el resto de los refinamientos e incluir el modelo completo en Rodin y
correrlo en ProB.
1
context ctx
sets
M EDICOS
axioms
f inite(M EDICOS)
end
machine hospital sees ctx
variables agentesM edicos
invariants
agentesM edicos ⊆ M EDICOS
EVENTS
initialisation
begin
agentesM edicos := ∅
end
event Activar
any am
where
am ∈ M EDICOS
am 6∈ agentesM edicos
then
agentesM edicos := agentesM edicos ∪ {am}
end
event Actividad
then
skip
end
event Desactivar
any am
where
am ∈ agentesM edicos
then
agentesM edicos := agentesM edicos\{am}
end
El primer refinamiento representa los pacientes. Al lllegar al hospital cada paciente
se asocia con un médico. La variable doctorAsignado modela esto. Dos eventos nuevos
2
representan la llegada y salida de un paciente del hospital.
context ctx2 extends ctx
sets
P ACIEN T ES
axioms
f inite(P ACIEN T ES)
end
3
machine Hospital1 refines Hospital sees ctx2
variables
agentesM edicos
pacientes, doctorAsignado, ultimaV isita, visitados
invariants
inv1 : pacientes ⊆ P ACIEN T ES
inv2 : doctorAsignado ∈ pacientes → agentesM edicos
inv3 : ultimaV isita ∈ pacientes →
7 M EDICOS
inv4 : visitados ⊆ pacientes
inv5 : ultimaV isita[visitados] ⊆ agentesM edicos
inv6 : visitados ⊆ dom(ultimaV isita)
EVENTS
initialisation extended
then
agentesM edicos := ∅
pacientes := ∅
doctorAsignado := ∅ultimaV isita := ∅
visitados := ∅
end
event ActivarAgente extends Activar
end
event LlegaP aciente =
any am pa
where
pa ∈ P ACIEN T ES ∧ pa 6∈ pacientes ∧ am ∈ agentesM edicos
then
pacientes := pacientes ∪ {pa}
doctorAsignado(pa) := am
end
event DescargueP aciente
any
pa
where
pa ∈ pacientes
pa 6∈ visitados
then
pacientes := pacientes\{pa}
doctorAsignado := {pa} C
− doctorAsignado
ultimaV isita := {pa} C
− ultimaV isita
end
...
4
event EmpiezaV isita refines Actividad
any am, pa
where am ∈ agentesM edicos ∧ pa ∈ pacientse ∧ pa 6∈ visitados ∧ am 6∈ ultimaV isita[visitados]
then
ultimaV isita(pa) := am
visitados := visitados ∪ {pa}
end
event f inalV isita extends Actividad
any
pa
where
pa ∈ visitados
then
visitados := visitados\{pa}
end
event saleAgente refines desactivar
any am
where
am ∈ agentesM edicos ∧ am 6∈ ran(doctorAsinado) ∧ am 6∈ ultimaV isita[visitados]
then
agentesM edicos := agentesM edicos\{ma}
end
event ReasigneDoctor refines desactivar
any am nuevo am
where
am ∈ ran(doctorAsignado) ∧ am 6∈ ultimaV isita[visitados]∧
nuevo am ∈ agentesM edicos ∧ nuevo am 6= am
then
agentesM edicos := agentesM edicos\{am}
doctorAsignado := doctorAsignado C
− (dom(doctorAsignado B {am}) × {nuevo am})
end
El evento Actividad modela el examen del paciente a la formulación de medicinas.
La variable visitados representa un subconjunto de los pacientes que están siendo examinados. La variable ultimaV isita guarda para cada paciente el último doctor que lo
visitó. Los eventos empiezaV isita y f inalV isita, refinan el evento actividad y modelan
el proceso de visita. El evento abstracto Desactivar se descompone en dos, saleAgente y
ReasigneDoctor. El evento saleAgente modela a un doctor que sale del hospital.
En la especificación de Hospital1, al definir los eventos saleAgente y ReasigneDoctor,
se hizo abstracción (es decir, no se modeló) de las razones para la salida del doctor y para
5
la reasignación de doctor a un paciente. Un doctor sale del hospital porque su jornada
terminó o porque el agente ha tenido una falla irrecuperable (recuerde que los agentes son
dispositivos) y debe ser desconectado.En un nuevo refinamiento debe distinguir entre la
salida normal de un agente y la desconexión.
En un sistema de múltiples agentes, los agentes pierden su conexión solamente por un
corto perı́odo. Después de que la conexión se restablece, el agente debe poder continuar su
operación. Por esto, después de detectar pérdida de conexión, no se debe inmediatamente
descartar el agente, sino más bien establecer un lı́mite para restablecer la conexión. Si el
agente restablece su conexión antes del lı́mite, puede entonces continuar su actividad. Sin
embargo, si no lo hace, se debe descartar permanentemente el agente. Para modelar este
comportamiento, debe en su refinamiento introducir una variable nueva desconectados
que representa los agentes activos que se ha detectado que han perdido conexión. Para
modelar el tiempo lı́mite, debe usar una variable reloj, para cada agente.. Inicialmente,
para todo agente activo, su reloj está en el estado inactivo. Tan pronto como el agente
pierde conexión, se agrega a los desconectados y su reloj se pone en activo. Debe haber un
evento que modela este caso. Debe tambier modelar dos eventos, uno para el caso en que el
agente logra reconectarse y otro para el que no lo logra. Si el agente se reconecta antes de
que su reloj esté en enLimite, el valor de reloj se reasigna a inactivo y el agente continua
su actividad. De lo contrario, el agente se elimina de los agentes activos.
Note que no hay realmente paso de tiempo. Simplemente uno de sus eventos supone
que el reloj del agente debe pasar a enLimite y el otro que debe pasar a inactivo. Note
también que debe refinar sus eventos reasigneDoctor y saleAgente para tener en cuenta
el caso de que el agente que se va o que se reasigna sea fallido (su reloj está en enLimite).
Es decir, tendrá dos eventos refinados para cada uno de estos. Uno para el caso normal y
otro para agentes fallidos.
Recuerde qe el invariante debe contener las propiedades de sus observaciones. Por ejemplo, una propiedad que dice que si el reloj de un agente no está en inactivo es porque ese
agente está desconectado.
Concretamente, su refinamiento debe:
1. Escribir un nuevo contexto, si hace falta
2. Escribir el nuevo invariante, incluyendo la propiedad: “si el reloj de un agente no
está en inactivo es porque ese agente está desconectado”
3. Modelar el reloj de cada agente
4. Refinar los eventos:
ActivarAgente
llegaP aciente
DescargueP aciente
6
EmpiezaV isita
f inalV isita
5. Refinar el evento saleAgente con dos eventos, uno para salida normal y otra para el
que detecta que quien sale es agente fallido
6. Refinar el evento ReasigneDoctor con dos eventos, como para el anterior.
7. Escribir un nuevo evento para desconectar un agente (pero no eliminarlo)
8. Escribir un nuevo evento para modelar que la reconexión falló.
9. Escribir un nuevo evento para modelar que la reconexión fue exitosa.
Debe considerar ahora un refinamiento adicional. En este se modelan llamadas de emergencia. Cada llamada de emergencia corresponde a un cierto tipo de alarma. Para cada
paciente que hace una llamada, se desea observar el paciente junto con el tipo de alarma
que se naló. Cada llamada la atiende un médico, aunque en un momento dado es posible
que haya llamadas que no hayan sido atendidas todavı́a. Se observa también el tipo de
alarma, junto con el doctor que la atiende. No puede haber dos médicos que atiendan la
misma llamada. Obviamente, no puede ser que un médico esté atendiendo una llamada que
ningn paciente haya hecho. No se puede descargar a un paciente que tenga una llamada de
emergencia pendiente. Tampoco puede resignares o salir un agente que tenga a su cargo
una llamada de emergencia. Además de refinar los eventos que se tenı́an, hay dos eventos nuevos, uno que corresponde a hacer una llamada de emergencia y otro para asignar
un médico a alguna llamada. Debe escribir este nuevo refinamiento, junto con un nuevo
contexto, si hace falta.
Una vez escrito todo el modelo en Rodin, debe correrlo con proB.
7