面向带数据与时间的异构系统协调与验证
软件工程
2025-08-19 v1
摘要
现代软件系统通常通过协调多个异构部分来实现，每个部分负责特定的任务。这些部分必须无缝协作以满足整体系统需求。为了验证此类复杂系统，我们开发了一个非侵入式协调框架，能够对交换数据并包含实时能力的异构部分进行形式化分析。该框架利用了一个语言扩展，该扩展被实现为一个中央代理和一种用于集成异构语言及协调各部分的领域特定语言。此外，抽象的规则模板被具体化为语言适配器，用于与代理进行非侵入式通信。该框架使用重写逻辑 (Maude) 实现，并通过验证一个异构公路-铁路道口系统的某些正确性属性来证明其适用性。
引用
@article{arxiv.2508.12325,
title = {Towards the Coordination and Verification of Heterogeneous Systems with Data and Time},
author = {Tim Kräuter and Adrian Rutle and Yngve Lamo and Harald König and Francisco Durán},
journal= {arXiv preprint arXiv:2508.12325},
year = {2025}
}
备注
This is the authors accepted version of a paper to be published in MODELS-2025, DOI: TBD