Formalizing TLM with Communicating State Machines
Formalizing TLM with Communicating State Machines
复制标题
通过通信状态机形式化 TLM
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
C. Haubelt
中科院分区：
文献类型：
--
作者：
B. Niemann;C. Haubelt
在嵌入式系统开发过程中，交易级别模型被广泛用作高级参考模型。高模拟速度和出色的建模灵活性是TLM成功的主要原因。虽然对于TLM设计人员来说，建模灵活性是可取的，但在模型的分析和验证过程中会产生问题。在本文中，我们通过引入一组规则来形式化事务级别模型的概念，这些规则允许将TLMS转换为一组通信状态机器。 Systemc是最受欢迎的TLM语言，我们还提出了SystemC调度程序的有限状态模型。最后，我们证明，使用我们的建模方法，可以使用标准模型检查器正式证明有限状态模型的属性。
Transaction Level Models are widely being used as high-level reference models during embedded systems development. High simulation speed and great modeling flexibility are the main reasons for the success of TLMs. While modeling flexibility is desirable for the TLM designer, it generates problems during analysis and verification of the model. In this paper we formalize the notion of Transaction Level Models by introducing a set of rules that allow the transformation of TLMs to a set of communicating state machines. SystemC being the most popular TLM language, we additionally present a finite state model of the SystemC scheduler. Finally, we demonstrate that using our modeling approach, a standard model checker can be employed to formally prove properties on the finite state model.