发表机构
University of Tehran; IT University of Copenhagen; University of Oslo; Mälardalen University; KTH（德黑兰大学; 哥本哈根信息技术大学; 奥斯陆大学; 马尔默达尔大学; 皇家理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种针对Timed Rebeca的静态切片等价性分析，证明其蕴含弱定时互模拟，从而在行为不变时重用微型孪生体，显著降低验证成本。
AI 中文摘要
微型孪生体是从定时Actor模型中为选定的可观察消息派生的紧凑行为模型。当源模型演化时，即使相关行为未改变，重新生成其微型孪生体也需要状态空间探索和约简。我们提出了一种针对Timed Rebeca的静态分析，该方法比较Rebeca依赖图中针对给定可观察消息名称集合的后向切片。对于带有after注解且无延迟语句的Zeno-free片段，我们证明了切片等价性意味着在选定观察下弱定时互模拟。这保留了内部转换中的可观察动作和总经过时间，从而允许重用现有的微型孪生体。我们在十个基准模型及其保持可观察切片的修订版本上评估了该实现。静态比较的成本取决于表示源语句及其依赖关系的图的大小，而微型孪生体生成则取决于可达状态和转换的数量。这一差异反映在测量结果中：静态比较使用数十兆字节内存，耗时不到一秒，而微型孪生体生成可能耗时超过一小时并使用数百吉字节内存。
英文摘要
Tiny twins are compact behavioral models derived from timed actor models for selected observable messages. When a source model evolves, regenerating its tiny twin requires state-space exploration and reduction even if the relevant behavior is unchanged. We present a static analysis for Timed Rebeca that compares backward slices of Rebeca dependence graphs for a given set of observable message names. For the Zeno-free fragment with after annotations and no delay statements, we prove that slice equivalence implies weak timed bisimulation under the selected observations. This preserves observable actions and total elapsed time across internal transitions, allowing the existing tiny twin to be reused. We evaluate the implementation on ten benchmark models paired with revisions that preserve their observable slices. The cost of static comparison depends on the size of the graphs representing source statements and their dependencies, while tiny-twin generation depends on the number of reachable states and transitions. This difference is reflected in the measurements: static comparison takes less than one second using tens of megabytes of memory, while tiny-twin generation can take over an hour and use hundreds of gigabytes.
Comments24 pages, 6 figures, 4 tables
