1425 - formal verification of space systems designed with taste (1).PDF