Ada and SPARK: Beyond Static Analysis for Medical Devices

The need for safe and secure software — including Medical Device software — is becoming more important as cybersecurity threats in the healthcare sector become more frequent and severe. Beyond increasing the reliability, safety and security of their software, Ada and SPARK programming language adopters are also looking at controlling and reducing costs. Hillrom migrated to Ada and SPARK to verify the safety of the code by formally proving some properties, and improving its efficiency by removing dynamic checks, all the while keeping development and verification costs down. Read the full case study to find out more.