Model checking usage policies†
Model checking usage policies†
复制标题
模型检查使用政策†
DOI：
--
复制
发表时间：
2009
影响因子：
0.5
通讯作者：
R. Zunino
中科院分区：
文献类型：
--
作者：
Massimo Bartoletti;P. Degano;G. Ferrari;R. Zunino
我们研究使用自动机，一个正式的模型，用于指定资源的使用政策。使用自动机扩展了有限状态自动机，增加了一些额外的特征，参数和保护，提高了它们的表达能力。我们表明，使用自动机的表达能力足以模拟现实世界中的应用程序的政策。我们讨论他们的表达能力，我们证明了这个问题告诉是否符合使用策略的计算是可判定的。本文的主要贡献是使用自动机的模型检测技术。该模型是使用模型，即描述资源访问和创建的可能模式的基本过程。尽管模型具有无限的状态，由于递归和资源创建，我们设计了一个多项式时间模型检查技术，用于确定何时使用符合使用策略。
We study usage automata, a formal model for specifying policies on the usage of resources. Usage automata extend finite state automata with some additional features, parameters and guards, that improve their expressivity. We show that usage automata are expressive enough to model policies of real-world applications. We discuss their expressive power, and we prove that the problem of telling whether a computation complies with a usage policy is decidable. The main contribution of this paper is a model checking technique for usage automata. The model is that of usages, i.e. basic processes that describe the possible patterns of resource access and creation. In spite of the model having infinite states, because of recursion and resource creation, we devise a polynomial-time model checking technique for deciding when a usage complies with a usage policy.