Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMRT/PacemakerRT/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Errors.out Sprache: VDM

Untersuchung VDM^©

\section{Lead class}

The Lead models a Pacemaker lead that read and write pulse values from
and to the heart. Each lead its attached to a specific chamber and this
is captured using the instance variable chamber.

\begin{vdm_al}
class Lead is subclass of GLOBAL

instance variables

private chamber : Chamber;
private scheduledPulse : [(Time * Pulse)];

operations

public
Lead: Chamber ==> Lead
Lead(chm) ==
   (
    chamber := chm;
    scheduledPulse := nil
   );
\end{vdm_al}

This is an auxiliar function that inspect the chamber where this lead is
attached to.

\begin{vdm_al}

public
getChamber: () ==> Chamber
getChamber () == return chamber;
\end{vdm_al}

Whenever theres an electrical pulse in that chamber the environment will
call the following stimulate operation.

\begin{vdm_al}

public
stimulate : Sense ==> ()
stimulate (s) == Pacemaker`heartController.sensorNotify(s,chamber);

\end{vdm_al}

\begin{vdm_al}
public
isFinished : () ==> ()
isFinished () == skip;

\end{vdm_al}

The following operation discharges a pulse to the heart.

\begin{vdm_al}
public
addLeadPace : Pulse * Time ==> ()
addLeadPace (p,t) ==
   if t <= time
   then dischargePulse(p,chamber)
   else (scheduledPulse := mk_(t,p);
         return);
\end{vdm_al}

\begin{vdm_al}
private
dischargePulse : Pulse * Chamber ==> ()
dischargePulse (p,c) ==
    duration(4)
    World`env.handleEvent(p,c,time);
\end{vdm_al}

\begin{vdm_al}
private
followPlan : () ==> ()
followPlan () ==
    (
     dcl curTime : Time := time;
     if scheduledPulse <> nil
     then if(curTime >= scheduledPulse.#1)
          then (dischargePulse(scheduledPulse.#2,chamber);
                scheduledPulse := nil);

   );


\end{vdm_al}

\begin{vdm_al}
thread
  periodic (50E6,0,49,0) (followPlan)

\end{vdm_al}

\begin{vdm_al}
sync

mutex(addLeadPace);
mutex(dischargePulse);
mutex(followPlan);
per isFinished =>  scheduledPulse = nil;

end Lead
\end{vdm_al}