定时I/O自动机：完善定时规范理论永不为迟
形式语言与自动机理论
2023-07-14 v2 软件工程
摘要
规范理论将规范与实现的概念同满足关系、精化关系以及支持逐步设计的一组算子相结合。我们基于定时I/O自动机作为规范形式，以定时I/O迁移系统表达语义，为实时系统开发了一套完整的规范框架。我们提供了精化、一致性检查、逻辑与结构组合以及规范商等构造——这些都是组合设计方法不可或缺的成分。该理论有严格的证明支撑，并正在开源工具ECDAR中实现。
引用
@article{arxiv.2302.04529,
title = {Timed I/O Automata: It is never too late to complete your timed specification theory},
author = {Martijn A. Goorden and Kim G. Larsen and Axel Legay and Florian Lorber and Ulrik Nyman and Andrzej Wasowski},
journal= {arXiv preprint arXiv:2302.04529},
year = {2023}
}
备注
Version submitted for review