Automatic coding from ZedCharts to SPARK Ada for safety-critical systems. - Feng Gang Shi (1995)