A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Shigeta KUNINOBU, Yoshiaki TAKATA, Naoya NITTA, Hiroyuki SEKI, "Policy Controlled System and Its Model Checking" in IEICE TRANSACTIONS on Information,
vol. E88-D, no. 7, pp. 1685-1696, July 2005, doi: 10.1093/ietisy/e88-d.7.1685.
Abstract: A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method.
URL: https://global.ieice.org/en_transactions/information/10.1093/ietisy/e88-d.7.1685/_p
Copy
@ARTICLE{e88-d_7_1685,
author={Shigeta KUNINOBU, Yoshiaki TAKATA, Naoya NITTA, Hiroyuki SEKI, },
journal={IEICE TRANSACTIONS on Information},
title={Policy Controlled System and Its Model Checking},
year={2005},
volume={E88-D},
number={7},
pages={1685-1696},
abstract={A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method.},
keywords={},
doi={10.1093/ietisy/e88-d.7.1685},
ISSN={},
month={July},}
Copy
TY - JOUR
TI - Policy Controlled System and Its Model Checking
T2 - IEICE TRANSACTIONS on Information
SP - 1685
EP - 1696
AU - Shigeta KUNINOBU
AU - Yoshiaki TAKATA
AU - Naoya NITTA
AU - Hiroyuki SEKI
PY - 2005
DO - 10.1093/ietisy/e88-d.7.1685
JO - IEICE TRANSACTIONS on Information
SN -
VL - E88-D
IS - 7
JA - IEICE TRANSACTIONS on Information
Y1 - July 2005
AB - A policy is an execution rule (or constraint) for objects in a system to retain security and integrity of the system. We introduce a simple policy specification language and define its operational semantics. A new NFA construction algorithm that works in linear time is proposed and a model checking method for policy controlled system (PCS) is presented. We conducted verification of a sample PCS for hotel reservation by our automatic verification tool and the experimental results showed the efficiency of the proposed method.
ER -