Using Formal Methods for Engineering Embedded Systems

Between 1985 and 1987, a radiation therapy device called the Therac-25 was involved in at least six incidents in which the device delivered massive overdoses of radiation. The patients involved suffered radiation burns and symptoms of radiation poisoning. Three of those patients eventually died, all because of a latent software bug. A race condition had gone undetected. It was a test case no one had thought to define.