Affiliations: Chair of Programming Systems, TU Dortmund, Germany | Chair of Service and Software Engineering, University of Potsdam, Germany | Carnegie Mellon University, Palo Alto, CA, USA
Abstract: 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.
