# A Model-Derivation Framework for Software Analysis

## TL;DR

This paper introduces an automated framework that derives behavioral models from Java programs, enabling high-level verification with improved consistency, scalability, and expressiveness for model-based software analysis.

## Contribution

The framework automates model derivation from Java bytecode, integrating transformations to produce timed automata suitable for model checking, enhancing efficiency and accuracy.

## Key findings

- Framework successfully derives models from real-sized Java programs.
- Models are consistent with original software behavior.
- Case studies validate scalability and expressiveness.

## Abstract

Model-based verification allows to express behavioral correctness conditions like the validity of execution states, boundaries of variables or timing at a high level of abstraction and affirm that they are satisfied by a software system. However, this requires expressive models which are difficult and cumbersome to create and maintain by hand. This paper presents a framework that automatically derives behavioral models from real-sized Java programs. Our framework builds on the EMF/ECore technology and provides a tool that creates an initial model from Java bytecode, as well as a series of transformations that simplify the model and eventually output a timed-automata model that can be processed by a model checker such as UPPAAL. The framework has the following properties: (1) consistency of models with software, (2) extensibility of the model derivation process, (3) scalability and (4) expressiveness of models. We report several case studies to validate how our framework satisfies these properties.