본문 바로가기
HOME> 논문 > 논문 검색상세

논문 상세정보

네트워크 기반 시스템 명세 및 검증을 위한 Z 프레임워크
Z based Framework for Networked System Specification and Verification

신지훈    (고려대학교 컴퓨터학과   ); 최진영    (고려대학교 컴퓨터학과   ); 강인혜    (서울시립대학교 기계정보공학과   ); 고병령    (한국원자력기술(주)  );
  • 초록

    정형명세 언어인 Z는 상태기반의 명세언어로써 시스템의 기능성을 명세 및 검증하는데 사용되고 있다. Z를 사용하여 시스템 명세 시 Z에서 제공하는 스키마를 이용하여 복잡한 구조의 상태를 나타내기에 용이하다. 하지만 Z에서 커버하는 명세 대상이 단일 시스템이기 때문에 2개 이상의 시스템으로 구성된 네트워크 상의 통신을 나타내기가 힘든 단점이 있다. 본 논문에서는 Z를 이용하여 네트워크 환경의 시스템들의 기능 및 통신을 명세하기 위한 프레임워크를 제시하고 사례연구를 통해 Z를 통해 시스템의 기능성 및 통신을 모두 명세하여 프레임워크의 적용가능성을 살펴본다. 또한 두 가지 측면을 모두 포함하는 검증 속성을 나타냄으로써 네트워크 환경 시스템의 속성을 프레임워크를 통해 명세, 검증 가능함을 보인다.


    Formal specification language Z is a state-based language and used for specifying and verifying system functionalities. By using Z for specifying system, developer can easily describe a complex state through a schema in Z but, the communication in network including more than two systems is not possible to be specified. In this paper, we propose the Z framework for representing communication and functionality of systems in a networked environment and show applicability of the framework by specifying both communication and functionality of safety critical real system, hydrogen monitoring system. The many properties which system must hold have functionality and communication simultaneously so in case study, we describe verification property including two aspects and show possibility of specifying and verifying properties in networked environment using framework.


  • 주제어

    정형기법 .   네트워크 시스템 명세 .   임베디드 시스템 명세 및 검증.  

  • 참고문헌 (7)

    1. Woodcock, Larsen, Bicarregui, Fitzgerald. "Formal Methods: Practice and Experience," ACM Comput. Surv., vol.41, no.4, 2009. 
    2. J.H.Lee et al., "Development of the Formal Requirements Specification of the Safety-critical Railway Systems," Journal of KIISE : Software and Applications, vol.35, no.9, pp.705-811, 2008.12. 
    3. Mike Spivey, "The Z Notaion : a reference manual, 2 edition," Prentice Hall, Englewood Cliffs, 1998. 
    4. Susan Stepney, David Cooper, Jim Woodcock, "An Electronic Purse Specification, Refinement, and Proof," Prentice Hall, Englewood Cliffs, 2000. 
    5. Roderick Chapman, "Correctness by construction: a manifesto for high integrity software," Proceedings of the 10th Australian workshop on Safety critical systems and software, vol.55, pp.43-46, 2006. 
    6. N,A. Zafar, "Formal Specification and validation of railway network components using Z notation," IET Softw., vol.3, Iss.4, pp.312-320, 2009. 
    7. David Basin, Ernst R. Olderog, and Paul E. Sevinc. Specifying and analyzing security automata using CSP-OZ. In ASIACCS '07: Proceedings of the 2nd ACM symposium on Information, computer and communications security, pp.70-81, New York, NY, USA, 2007. 

 저자의 다른 논문

  • 신지훈 (3)

    1. 2013 "안전 필수 시스템의 정형기법 적용 - 원자력 시스템과 철도 제어 시스템 사례연구" 정보과학회지 = Communications of the Korean Institute of Information Scientists and Engineers 31 (5): 46~55    
  • 최진영 (82)

  • 강인혜 (7)

  • 고병령 (2)

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

무료다운로드
유료다운로드

유료 다운로드의 경우 해당 사이트의 정책에 따라 신규 회원가입, 로그인, 유료 구매 등이 필요할 수 있습니다. 해당 사이트에서 발생하는 귀하의 모든 정보활동은 NDSL의 서비스 정책과 무관합니다.

원문복사신청을 하시면, 일부 해외 인쇄학술지의 경우 외국학술지지원센터(FRIC)에서
무료 원문복사 서비스를 제공합니다.

NDSL에서는 해당 원문을 복사서비스하고 있습니다. 위의 원문복사신청 또는 장바구니 담기를 통하여 원문복사서비스 이용이 가능합니다.

이 논문과 함께 출판된 논문 + 더보기