Formal validation and verification of a medical software critical component