Modelling and Verifying Contract-Oriented Systems in Maude
Modelling and Verifying Contract-Oriented Systems in Maude
复制标题
在 Maude 中建模和验证面向合同的系统
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
R. Zunino
中科院分区：
文献类型：
--
作者：
Massimo Bartoletti;Maurizio Murgia;A. Scalas;R. Zunino
我们解决了建模和验证面向合同的系统的问题，在该系统中，分布式代理可能会通告和规定合同，但与大多数其他分布式代理方法不同的是，并不假设总是“诚实”地行为。我们用Maude描述了面向契约的系统的演算CO2的语义的可执行规范[6]。诚实属性[5]是那些在所有可能的执行环境中始终遵守合同的代理人的特征。由于存在无限数量的这样的上下文，因此不能通过对代理的状态空间进行模型检查来直接验证诚实(实际上，诚实通常是一个无法确定的属性[5])。本文的主要贡献是提出了一种可靠的真实性验证技术。要做到这一点，我们通过从流程可能涉及的实际上下文中抽象出来，安全地过度近似诚实属性。然后，我们为这种抽象开发了一种模型检测技术，我们描述了一个在Maude中的实现，并讨论了一些实验。
We address the problem of modelling and verifying contract-oriented systems, wherein distributed agents may advertise and stipulate contracts, but — differently from most other approaches to distributed agents — are not assumed to always behave “honestly”. We describe an executable specification in Maude of the semantics of CO2, a calculus for contract-oriented systems [6]. The honesty property [5] characterises those agents which always respect their contracts, in all possible execution contexts. Since there is an infinite number of such contexts, honesty cannot be directly verified by model-checking the state space of an agent (indeed, honesty is an undecidable property in general [5]). The main contribution of this paper is a sound verification technique for honesty. To do that, we safely over-approximate the honesty property by abstracting from the actual contexts a process may be engaged with. Then, we develop a model-checking technique for this abstraction, we describe an implementation in Maude, and we discuss some experiments with it.
打字诚实
影响因子：
0.6
作者：
Bartoletti M
通讯作者：
Bartoletti M