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