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

논문 상세정보

HDTL을 이용한 병렬 자바 프로그램의 모니터 링과 검사
Monitoring and Checking Concurrent Java Programs with HDTL

조승모   (한국과학기술원 첨단정보기술연구센터UU0001375  ); 김형호   (한국과학기술원 전산학과UU0001375  ); 차성덕   (한국과학기술원 전산학과UU0001375  ); 배두환   (한국과학기술원 전산학과UU0001375  );
  • 초록

    정형 명세를 이용하여 구현된 프로그램이 수행 중에 명세를 만족시키는지 모니터링하고 검사하는 기법에 대한 연구들이 기존에 많이 수행되어 왔다. 이들은 주로 요구사항 명세언어로 시제논리 혹은 그것의 확장을 사용하게 된다. 이때 대부분의 연구는 실제 구현된 시스템이 가지는 동적인 변화를 제대로 요구사항 명세에 기술하고, 검사할 수 있는 언어를 제공하지 못하고 있다. 본 연구에서는 동적 시스템의 특성 명세언어로 기존에 제안했던 HDTL을 사용하여 동적인 자바 프로그램의 수행을 모니터링하고 검사하는 프레임웍을 제안한다.


    There have been many researches about monitoring and checking the implementations during run-time using formal requirement specification. They usually adopt temporal logics or their extensions to specify the requirements for the implementations. However, most of the systems fail to support the specification of requirements fir dynamic systems - systems whore components are created and removed during run-time. Unlike analysis or design models, most actual implementations are dynamic, so the notion of instances should be employed in the property specification language. In this paper, we show how we can monitor and check Java programs using our temporal logic for dynamic systems (HDTL). We suggest a framework in which the execution of Java programs are monitored and chocked against given HDTL requirements.


  • 주제어

    정형 명세 .   동적 시스템 검증 .   자바.  

  • 참고문헌 (10)

    1. M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, and J. Quesada, 'Maude: Specification and Programming in Rewriting Logic,' Maude System documentation, March, 1999 
    2. http://java.sun.com/j2se/1.3/docs/guide/jpda/ 
    3. Hsiang, J., 'Refutational Theorem Proving using Term Rewriting Systems,' PhD thesis, University of Illinois at Champaign-Urbana, 1981 
    4. Cohen, S., Jtrek. Compaq, http://www.compaq.com/java/download/jtrek 
    5. Laura K. Dillon and Y. S. Ramakrishna, 'Generating oracles from your favorite temporal logic specifications,' Proceedings of the Fourth ACM SIGSOFT Symposium on Foundations of Software Engineering, Oct. 1996 
    6. Seung Mo Cho, Hyung Ho Kim, Sung Deok Cha and Doo Hwan Bae, 'Specification and Validation of Dynamic Systems using Temporal Logic,' IEE Proceedings-Software, Vol. 148, No 4, Aug. 2001 
    7. M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan, 'Java-Mar': a Run-time Assurance Tool for Java Programs,' Proc. First Workshop on Runtime Verification (RV'01), Paris, France, 23 July 2001 
    8. Klaus Havelund, Grigore Rosu, 'Monitoring Java Programs with Java PathExplorer,' Proc. First Workshop on Runtime Verification(RV'01), Paris, France, 23 July 2001 
    9. Dietrich, F., Logean, X.. Koppenhofer, S. & Hubaux, J. - P., 'Modelling and testing object-oriented distributed systems with linear-time temporal logic,' Technical Report SSC/1998/011, Swiss Federal Institute of Technology, Lausanne 
    10. A. Pnueli, 'The temporal logic of programs,' Proc. 18th IEEE Symposium on Foundation of Computer Science, 1977 

 저자의 다른 논문

  • 조승모 (4)

    1. 1999 "LUSTRE를 이용한 SCR 명세의 구현" 정보과학회논문지. Journal of KISS (b):software and applications. B 26 (2): 251~262    
    2. 2000 "병렬 객체지향 시스템의 검증" 정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용 27 (1): 1~12    
    3. 2002 "동적 시스템 명세를 위한 시제논리언어와 그 검증" 정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용 29 (7): 450~464    
  • 김형호 (6)

  • 차성덕 (29)

  • 배두환 (35)

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

무료다운로드
  • NDSL :
유료다운로드

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

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

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

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