Earticle

현재 위치 Home

A Formal Verification Method of Obligation Policy in Multi-agent System

첫 페이지 보기
  • 발행기관
    보안공학연구지원센터(IJUNESST) 바로가기
  • 간행물
    International Journal of u- and e- Service, Science and Technology 바로가기
  • 통권
    Vol.8 No.11 (2015.11)바로가기
  • 페이지
    pp.113-124
  • 저자
    Zhang Tao, Xie Hong, Huang Shao-bin
  • 언어
    영어(ENG)
  • URL
    https://www.earticle.net/Article/A270162

※ 원문제공기관과의 협약기간이 종료되어 열람이 제한될 수 있습니다.

원문정보

초록

영어
In Multi-Agent System, obligations are actions that agents are required to take or some states of affairs which should be maintained, formal modeling and verifying obligation policy which is high-level requirements specifications or communication protocol for constraining agent interaction can enhance the correctness of the system design. In this paper, we present a formal framework for modeling obligation policy, the framework is formalized using concepts of social commitments, it allows reasoning about change in the states of obligations and provides Kripke operational semantics which can help to convert framework of obligation policy to the input model of model checker MCMAS, at the same time ,the properties of framework depending on policy conflicts are represented with CTL, and the violations of properties is detected by using MCMAS which can provide the counterexample and trace it back to the errors in interaction policy. Finally, we present an implementation and report on experimental results of verifying obligation policy using MCMAS model checker.

목차

Abstract
 1. Introduction
 2. Social Commitment
 3. Obligation Policy Language Model
  3.1. Obligation Policy Language
  3.2. Obligation Types
  3.3. State Model of Obligation
  3.4. The Formal Semantics of OPL
 4. Model Checking Interaction Policy
  4.1. OPL Model to ISPL Model
  4.2. The Properties of OPL Model
 5. A Case Study
  5.1. Model Obligation Policy
  5.2. Implementation of the Case Study
 6. Conclusions
 References

키워드

Multi-Agent System Model Checking obligation policy formal method MCMAS

저자

  • Zhang Tao [ College of Computer Science and Technology, Harbin Engineering University, Harbin, China ]
  • Xie Hong [ College of Information and Communication Engineering, Harbin Engineering University, Harbin, China ]
  • Huang Shao-bin [ College of Computer Science and Technology, Harbin Engineering University, Harbin, China ]

참고문헌

자료제공 : 네이버학술정보

간행물 정보

발행기관

  • 발행기관명
    보안공학연구지원센터(IJUNESST) [Science & Engineering Research Support Center, Republic of Korea(IJUNESST)]
  • 설립연도
    2006
  • 분야
    공학>컴퓨터학
  • 소개
    1. 보안공학에 대한 각종 조사 및 연구 2. 보안공학에 대한 응용기술 연구 및 발표 3. 보안공학에 관한 각종 학술 발표회 및 전시회 개최 4. 보안공학 기술의 상호 협조 및 정보교환 5. 보안공학에 관한 표준화 사업 및 규격의 제정 6. 보안공학에 관한 산학연 협동의 증진 7. 국제적 학술 교류 및 기술 협력 8. 보안공학에 관한 논문지 발간 9. 기타 본 회 목적 달성에 필요한 사업

간행물

  • 간행물명
    International Journal of u- and e- Service, Science and Technology
  • 간기
    격월간
  • pISSN
    2005-4246
  • 수록기간
    2008~2016
  • 십진분류
    KDC 505 DDC 605

이 권호 내 다른 논문 / International Journal of u- and e- Service, Science and Technology Vol.8 No.11

    피인용수 : 0건 (자료제공 : 네이버학술정보)

    함께 이용한 논문 이 논문을 다운로드한 분들이 이용한 다른 논문입니다.

      출처 : 네이버학술정보

        0개의 논문이 장바구니에 담겼습니다.

        페이지 저장
        소속기관 조회
        이용자님의 소속기관(단체)이 서비스에 가입되어 있는지 확인해 보십시오.
        기관회원에 소속되어 있는 이용자는 원문을 무료로 이용할 수 있습니다.