Simplifying translation validation via model extrapolation

We revisit our case study on the NASA's Voyager space mission to automatically discover its behaviour by means of model transformation and automata learning. We investigate the conformance of three structurally different types of specification of the case study: (1) a formal specification given in ASSL, (2) a derived implementation in Java, and (3) two behavioral models, one derived from the ASSL specification and one learned from the Java implementation. This way we show that Behavioural Mining, that extracts directly analyzable behavioural models from other artifacts (specifications or code) is a practicable and very simple way to obtain a process-oriented description of third-party systems. As the learning technique can be tailored to different abstraction levels according what behavioural primitives we decide to observe, we show and discuss different alternative learned models. This process oriented description is directly amenable to formal verification, as we show here by means of model checking.