期刊
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
卷 121, 期 -, 页码 101-115出版社
ELSEVIER SCIENCE BV
DOI: 10.1016/j.entcs.2004.10.010
关键词
opacity; non-deducibility; Petri nets; observable behaviour
资金
- EPSRC GOLD and SCREEN projects
- DSTL
We consider opacity as a property of the local states of the secure (or high-level) part of the system, based on the observation of the local states of a low-level part of the system as well as actions. We propose a Petri net modelling technique which allows one to specify different information flow properties, using suitably defined observations of system behaviour. We then discuss expressiveness of the resulting framework and the decidability of the associated verification problems.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据