The HiVY Tool Set

Our aim is to validate mission-specific components of spacecraft flight software designs that are specified using state-charts and translated automatically to the final flight code for the mission. We established an automatic translation tool set from state-charts to SPIN for the validation of such mission-specific components. To guarantee compliance with autogenerated flight code, our translation tool set preserves the StateFlow@ semantics. We are now able to specify and validate portions of mission-critical software design and implementation using the exhaustive exploration techniques of model checking.