Information Technology Reference
In-Depth Information
translated into Perfect Developer. We also automatically generated C# code
from the verified specification in less than five seconds. The refinement resulted
in over 9000 lines of verified C# code
2
. The choice of C# was due to the fact
that the interface between hand-written code and the code generated by Perfect
Developer is easier for C# than for other languages. Besides, C# provides tools
that makes it faster to develop a GUI for the pacemaker system. In Figure 3
we illustrate our graphical user interface of the pacemaker developed using C#
under
Microsoft Visual C# 2010
.
Fig. 3.
Pacemaker GUI using C#
According to its requirements [13], the pacemaker must be able to print re-
ports of the events occurred during the therapy. We modelled those reports in Z
by creating schema operations using output variables (those followed by an excla-
mation mark '!'). As an example, we present the operation
OutputActualTime
,
which simply outputs the actual value of the time in the
PulseGenerator
state.
For output operations, we include the predicate
Ξ
PulseGenerator
, instead of
Δ
PulseGenerator
, to assure that the operation does not change the state of the
system.
2
Available at http://sites.google.com/site/pacemakerinz/pacemaker-in-csharp.zip
Search WWH ::
Custom Search