Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Semi-Automatic Extraction of Formal Models from Object Oriented Code

P. H. M. van Spaendonck

TL;DR

This work provides a framework for transforming object-oriented code into processes from which, when paired with minimal user input, models can be automatically generated and composed, and introduces the novel SSTraGen (StateSpace Transformation&Generation) tool, which provides an implementation of this framework.

Abstract

Behavioral models are incredibly useful for understanding and validating software. However, the automatic extraction of such models from actual industrial code remains a largely unsolved problem with current solutions often not scaling well with the complexity and size of industrial systems or having to rely on approximations. To enable the extraction of useful models from code, we provide a framework for transforming object-oriented code into processes from which, when paired with minimal user input, models can be automatically generated and composed. Paired with this, we introduce the novel SSTraGen (StateSpace Transformation & Generation) tool, which provides an implementation of this framework. Through case studies at Philips Image Guided Therapy Systems, we showcase the practical applicability and usefulness of this tool, including the transformation of a component with >1000 LOC.

Semi-Automatic Extraction of Formal Models from Object Oriented Code

TL;DR

This work provides a framework for transforming object-oriented code into processes from which, when paired with minimal user input, models can be automatically generated and composed, and introduces the novel SSTraGen (StateSpace Transformation&Generation) tool, which provides an implementation of this framework.

Abstract

Behavioral models are incredibly useful for understanding and validating software. However, the automatic extraction of such models from actual industrial code remains a largely unsolved problem with current solutions often not scaling well with the complexity and size of industrial systems or having to rely on approximations. To enable the extraction of useful models from code, we provide a framework for transforming object-oriented code into processes from which, when paired with minimal user input, models can be automatically generated and composed. Paired with this, we introduce the novel SSTraGen (StateSpace Transformation & Generation) tool, which provides an implementation of this framework. Through case studies at Philips Image Guided Therapy Systems, we showcase the practical applicability and usefulness of this tool, including the transformation of a component with >1000 LOC.

Paper Structure

This paper contains 15 sections, 18 equations, 10 figures.

Table of Contents

  1. introduction
  2. Related Work
  3. From Code to Model
  4. Introduction to Process Algebra
  5. From Data Structure to Model
  6. From Code to Data Structure
  7. The SSTraGen tool
  8. Bounds
  9. Global namespace
  10. Command Line Interface
  11. Case study
  12. Conclusion & Future Work
  13. Process Semantics
  14. Implementation Details of the SSTraGen Tool
  15. Language generic transformation process

Figures (10)

  • Figure 1: Framework for transforming object-oriented code into behavioral models
  • Figure 2: (\ref{['fig:pseudocode_actuator']}) Actuator example code, (\ref{['fig:actuator_model']}) Model of the example code.
  • Figure 3: The SCPP language and associated sub-languages and data-types.
  • Figure 4: This diagram presents an abstract overview of the processes described in this section.
  • Figure 5: Example code that implements a moving platform.
  • ...and 5 more figures

Theorems & Definitions (9)

  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Definition 3.5
  • Definition 3.6
  • Definition 3.7
  • Definition 3.8
  • Definition A.1