Information Technology Reference
In-Depth Information
Quality Research Laboratory at McMaster University. Another interesting piece
of future work is to create some test scenarios to validate our system.
In the long term agenda, we intend to formalise the translation from Z to Per-
fect Developer. Besides guaranteeing the correction of the translation presented
in this paper, this formalisation can be used as a guideline in the implementation
of a tool that mechanises the translation. Moreover, a test suite could be used
in order to improve confidence of the translation. Yet another piece of interest-
ing work for the long term is to extend our model to include concurrency using
Circus
specifi-
cation into code using its refinement calculus and tool support [10]. Notions of
real-time are also to be incorporated in our model in a later stage using
[6], a combination of Z and CSP, and the derivation of the
Circus
Circus
'
timed version [21].
Acknowledgments
Jim Woodcock originally proposed this challenge. David Crocker gave an very
good support and kindly reduced the limitations of the Perfect Developer free
edition. INES and CNPq partially supports the work of the authors: grants
550946/2007-1, 620132/2008-6, 573964/2008-4, and 476836/2009-3.
References
1. Software Quality Research Laboratory SQRL (2008),
http://www.cas.mcmaster.ca/sqrl/
2. Carter, G., Monahan, R., Morris, J.M.: Software Refinement With Perfect Devel-
oper. In: SEFM 2005: Proceedings of the Third IEEE International Conference on
Software Engineering and Formal Methods, Washington, DC, USA, pp. 363-373.
IEEE Computer Society, Los Alamitos (2005)
3. Cavalcanti, A., Woodcock, J.: ZRC - A Refinement Calculus for Z. Formal Aspects
of Computing 10(3), 267-289 (1998)
4. Celoxica. Handel-C language reference manual, v3.0 (2002)
5. Boston Scientific Corporation. ALTRUA Pacemaker System Guide (2008)
6. de Oliveira, M.V.M.: Formal Derivation of State-Rich Reactive Programs Using
Circus PhD thesis, Department of Computer Science, University of York (2005)
YCST-2006/02
7. Ellenbogen, K.A., Wood, M.A.: Cardiac Pacemakers and ICDs. Wiley-Blackwell
(2005)
8. Gomes,
A.O.,
de
Oliveira,
M.V.M.:
Pacemaker
Specification
in
Z
Using
ProofPower-Z
9. Gomes, A.O., de Oliveira, M.V.M.: Formal Specification of a Cardiac Pacing Sys-
tem. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 692-707.
Springer, Heidelberg (2009)
10. Gurgel, A.C., Castro, C.G., de Oliveira, M.V.M.: Tool Support for the Circus
Refinement Calculus. In: B¨orger,E.,Butler,M.,Bowen,J.P.,Boca,P.(eds.)ABZ
2008. LNCS, vol. 5238, p. 349. Springer, Heidelberg (2008)
11. Hoare, T.: The Verifying Compiler: A Grand Challenge for Computing Research.
Journal of the ACM 50 (2003)
 
Search WWH ::




Custom Search