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

Angebot Produkte kleine Reime Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Windows-Programme und andere Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/VDM/VDMSL/pacemakerSL/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 13.4.2020 mit Größe 3 kB

Quellcode-Bibliothek RateController.vdmsl Sprache: VDM

\section{XXXR modes requirements}

The modes ending in R like AOOR require that we adjust the rate for that we had to model the component that will adjust the rate.

\paragraph{Programmable parameters requirements}

In this mode the following programmable parameters must be taken into account
while pacing:

\begin{itemize}
\item LRL shall be 60 ppm.
\item MSR shall be 120 ppm.
\item ActivityThreshold shall be \textbf{Med}.
\item ResponseFactor shall be 8.
\item ReactionTime shall be 30 s.
\item RecoveryTime shall be 5 m.
\end{itemize}

\paragraph{Purpose and abstraction level}

The rate controller full functionality is not modelled, we represent all the variables needed to control the increase and decrease in rate. But the changes will be instantaneous disregarding the response and recovery time delays. These are requirements for the rate change and not for the operating mode.

The purpose it to understand the different operation modes not how the rate changes, so its logical that if the rate can change on an operation mode for instance AOOR we model that change but in an abstract way.

\subsection*{VDM-SL module}

The rate controller will accept as input a sequence of Accelerometer inputs:

\begin{vdm_al}
module RateController

definitions

types

Input = map Time to ActivityData;
\end{vdm_al}

Activity data is mapped to a subset of nat1 as:

\begin{itemize}
\item{V-LOW} 1
\item{LOW} 2
\item{MED-LOW} 3
\item{MED} 4
\item{MED-HIGH} 5
\item{HIGH} 6
\item{V-HIGH} 7
\end{itemize}

Time is abstracted as a nat.

\begin{vdm_al}
Time = nat1;

ActivityData = nat1
inv a == a <= 7;

\end{vdm_al}

The response factor is an integer number betwen 1 and 16.

\begin{vdm_al}
RF = nat1
inv rf == rf <= 16;
\end{vdm_al}

The reaction of our system will be a comand to change the rate, in this case
we model the ouput as

\begin{vdm_al}

Output = map Time to PPM;

PPM = nat1
inv ppm == ppm >= 30 and ppm <= 175;

\end{vdm_al}

The programmable parameters are declared as values.

\begin{vdm_al}
values
   LRL           : PPM = 60;
   MSR           : PPM = 120;
   Threshold     : ActivityData = 6;
   ReactionTime  : Time = 150;
   ResponseFactor: RF = 8; -- Not understood
   RecoveryTime  : Time = 5;
\end{vdm_al}

Finally the simulation of the rate controller follows as a relation between the reach of the MSR with a exceeding input value of the treshold, and the LRL as a decrease after the reacovery time form the MSR or the normal functioning of the system.

\begin{vdm_al}
functions

Simulate(inp : Input)  out : Output
pre 0 not in set dom inp
post forall t in set dom inp &
            (out(t) = MSR =>  inp(t-ReactionTime) > Threshold or out(t-1) = MSR)
     and
     forall t in set dom inp \ {1} &
            (out(t) = LRL =>  inp(t-RecoveryTime) < Threshold or out(t-1) = LRL);

end RateController
\end{vdm_al}

\subsection{Requirements review}

\begin{itemize}
\item LRL \textbf{Modelled}.
\item MSR \textbf{Modelled}.
\item ActivityThreshold \textbf{Modelled}.
\item ResponseFactor \textbf{Not understood}.
\item ReactionTime \textbf{Modelled}.
\item RecoveryTime \textbf{Modelled}.
\end{itemize}

quality89%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.14Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.