从面向对象代码中半自动提取形式化模型
软件工程
2024-11-20 v1 形式语言与自动机理论
摘要
行为模型对于理解和验证软件非常有用。然而，从实际工业代码中自动提取此类模型在很大程度上仍是一个未解决的问题，目前的解决方案通常无法很好地适应工业系统的复杂性和规模，或者不得不依赖近似。为了能够从代码中提取有用的模型，我们提供了一个将面向对象代码转换为进程的框架，当结合最少的用户输入时，可以从这些进程中自动生成并组合模型。与此相配合，我们引入了新颖的 SSTraGen（StateSpace Transformation & Generation）工具，该工具提供了该框架的实现。通过在 Philips Image Guided Therapy Systems 的案例研究，我们展示了该工具的实际适用性和实用性，包括对包含 >1000 LOC 的组件的转换。
引用
@article{arxiv.2411.12386,
title = {Semi-Automatic Extraction of Formal Models from Object Oriented Code},
author = {P. H. M. van Spaendonck},
journal= {arXiv preprint arXiv:2411.12386},
year = {2024}
}