From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study | IEEE Conference Publication | IEEE Xplore