基于主动对象的形式系统模型原型化
Prototyping Formal System Models with Active Objects
摘要：
我们提出主动对象语言作为分布式系统的正式系统模型的开发工具。除了一个长期重写系统的基础上的形式化，我们使用建立软件工程的概念，包括软件产品线和面向对象的广泛的工具支持。我们说明了我们的建模方法的原型弱内存模型。由此产生的可执行模型是模块化的，并通过面向对象建模在通信参与者之间具有清晰的接口。基本内存模型的松弛表示为软件产品线的自包含变体。作为一种建模语言，我们使用正式的主动对象语言ABS，它带有一个广泛的工具集。这允许快速形式化的核心思想，早期的有效性检查方面的正式不变的证明，并通过执行测试运行调试支持。因此，我们的方法支持原型的正式系统模型与早期反馈。
英文摘要：
We propose active object languages as a development tool for formal system models of distributed systems. Additionally to a formalization based on a term rewriting system, we use established Software Engineering concepts, including software product lines and object orientation that come with extensive tool support. We illustrate our modeling approach by prototyping a weak memory model. The resulting executable model is modular and has clear interfaces between communicating participants through object-oriented modeling. Relaxations of the basic memory model are expressed as self-contained variants of a software product line. As a modeling language we use the formal active object language ABS which comes with an extensive tool set. This permits rapid formalization of core ideas, early validity checks in terms of formal invariant proofs, and debugging support by executing test runs. Hence, our approach supports the prototyping of formal system models with early feedback.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
