Simplifying Translation Validation via Model Extrapolation

Article type: Research Article

Authors: Howar, Falk^; | Margaria, Tiziana | Wagner, Christian

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

Note: [] Corresponding author. Email: falk.howar@tu-dortmund.de

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.

Keywords: Translation validation,, automata learning, model extraction, legacy software, simplicity, behavioural mining

DOI: 10.3233/jid-2013-0022

Journal: Journal of Integrated Design and Process Science, vol. 17, no. 3, pp. 71-91, 2013