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

논문 상세정보

스테이트차트의 실시간 검증을 위한 모델체커의 확장
Extending Model Checker for Real-time Verification of Statecharts

방호정   (KAIST 전자전산학과UU0001375  ); 홍형석  김태효   (KAIST 전자전산학UU0001375  ); 차성덕   (KAIST 전자전산학과UU0001375  );
  • 초록

    본 연구는 스테이트차트의 실시간 검증을 위한 알고리즘을 제안한다. 스테이트차트는 실시간 반응형 시스템의 명세에 많이 사용되고 있으며 동기적과 비동기적인 두개의 시간모델을 지원한다. 그러나 기존의 스테이트차트에 대한 실시간 검증 방법은 비동기적 시간 모델과 호환되지 않거나, 변수를 모델에 추가함으로써 모텔의 상태 공간을 증가시키는 단점이 있었다. 우리는 기존의 모델 체킹 알고리즘을 확장하여 이러한 문제점을 해결하였다. 확장된 알고리즘은 시간을 증가시키는 전이만을 고려하기 때문에 스테이트차트의 두 가지 시간 모델에 모두 사용할 수 있으며, 시간의 계산이 알고리즘 내부적으로 이루어지기 때문에 모델에 변수를 추가할 필요가 없어 상태공간을 증가시키지 않는다. 본 연구는 이러한 알고리즘을 토대로 기존의 모델 체커인 NuSMV를 확장하였으며, 사례 연구를 통하여 그 유용성을 확인하였다.


    This paper presents a method for real-time verification of Statecharts. Statecharts has been widely used for real-time reactive systems, and supports two time models: synchronous and asynchronous. However, existing real-time verification methods for them are incompatible with the asynchronous time model or increase state space by introducing new variables to the target models. We solved these problems by extending existing model checking algorithms. The extended algorithms can be used with both time models of Statecharts because they consider time increasing transitions only. In addition, they do not increase target state space since they count those transitions internally without additional variables. We extended an existing model checker, NuSMV, based on the proposed algorithms and conducted some experiments to show their advantage.


  • 주제어

    스테이트차트 .   실시간 검증 .   심볼릭 모델 체킹 .   정형 기법.  

  • 참고문헌 (21)

    1. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model Checking: 10 20 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 1-33, Washington, D.C., 1990. IEEE Computer Society Press 
    2. R. Alur, C. Courcoubetis, and D. Dill. Modelchecking for real-time systems. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 414-425, Philadelphia, 1990 
    3. G. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 35(5):279-295, 1997 
    4. William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon Damon Reese. Model checking large software specifications. Software Engineering, 24(7):498-520, 1998 
    5. N. Leveson, M. Heimdahl, H.Hildreth, and J.Reese. Requirements specification for process-control systems. IEEE Transactions on Software Engineering, 20(9), 1994 
    6. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244-263, 1986 
    7. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999 
    8. Sergio Campos, Marcia Teixeira, Marius Minea, Edmund Calrke, and Andreas Kuehlmann. Model checking semi-continuous time models using bdds. In Proceedings of the International Workshop on Symbolic Model Checking, 1999 
    9. H.J, Bang. Extending SMV for Real-time Verification of Statecbarts. Master's thesis, Korea Advanced Institute of Science and Technology, 2003 
    10. K. McMillan. Symbolic Model Checking. Kluwer, 1993 
    11. Sergio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, and Marius Minea. Verus: A tool for quantitative analysis of finite-state real-time systems. In Workshop on Languages, Compilers and Tools for Real-Time Systems, pages 70-78, 1995 
    12. Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, and Marco Roveri. NUSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4): 410-425, 2000 
    13. Pnueli A. A temporal logic of programs. Theoretical Computer Science, 13:45-60, 1981 
    14. David Harel and Amnon Naamad. The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4):293-333, 1996 
    15. Udo Brockmeyer and Gunnar Wittich. Real-time verification of STATEMATE designs. In Lecture Notes in Computer Science, pages 537-541, 1998 
    16. Udo Brockmeyer and Gunnar Wittich. Tamagotchis need not die-verification of STATEMATE designs. Tools and Algorithms for the Construction and Analysis of Systems(TACAS'98), 1998 
    17. S. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Proceedings of the Real-Time Systems Symposium. IEEE Computer Society Press, December 1994 
    18. S. Campos, E. Clarke, and M.Minea. The verus tool: A quantitative approach to the formal verification of real-time systems. In O. Grumberg, editor, Proc. 9th International Conference on Computer Aided Verifiauion (CAV'97), volume 1254, pages 452-455. Springer Verlag, 1997 
    19. E. Allen Emerson, A.K. Mok, A.P. Sistla, and Jai Srinivasan. Quantitative temporal reasoning. In Lecture Notes in Computer Science, volume 531, pages 136-145, 1990 
    20. D Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231-274, 1987 
    21. S.V. Campos and E. Clarke. Real-Time Symbolic Model Checking for Discrete Time Models. In T. Rus and C. Rattray, editors, Theories and Experiences for Real-Time System Development. World Scientific Press, AMAST Series in Computing, 1994 

 저자의 다른 논문

  • 차성덕 (29)

    1. 1995 "보안 제품 평가 기준 및 평가제도의 현황과 추세" 정보과학회지 = Communications of the Korean Institute of Information Scientists and Engineers 13 (11): 55~67    
    2. 1997 "지킴이: 유닉스 시스템을 위한 통합 보안 점검 도구" 通信情報保護學會論文誌 = Journal of the Korea Institute of Information Security and Cryptology 7 (3): 23~40    
    3. 1999 "LUSTRE를 이용한 SCR 명세의 구현" 정보과학회논문지. Journal of KISS (b):software and applications. B 26 (2): 251~262    
    4. 1999 "SCR 요구사항 명세의 정형적인 의미론" 정보과학회논문지. Journal of KISS (b):software and applications. B 26 (8): 988~999    
    5. 1999 "CPN 모델의 역방향 안전성 분석 도구 개발" 정보과학회논문지. Journal of KISS (c) : computing practices. C 5 (4): 457~466    
    6. 1999 "시스템 보안 강화를 위한 로그 분석 도구 ILVA와 실제 적용 사례" 通信情報保護學會論文誌 = Journal of the Korea Institute of Information Security and Cryptology 9 (3): 13~26    
    7. 2000 "복합 실시간 계통의 요구사항 명세와 안전성 분석을 위한 정성적 정형기법" 정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용 27 (2): 120~133    
    8. 2000 "페트리네트 Slice를 이용한 페트리네트 모델의 합성적 분석" 정보과학회논문지. Journal of KIISE. 소프트웨어 및 응용 27 (3): 210~216    
    9. 2000 "MSCTest: 내장 소프트웨어 테스트를 위한 자동화 도구" 정보과학회논문지. Journal of KISS : Computing practices. 컴퓨팅의 실제 6 (2): 187~195    
    10. 2001 "실시간 모델 체커를 이용한 폴리 트리의 체계적 검증" 소프트웨어공학회지 = Software engineering review 14 (1): 4~18    

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

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

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

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

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

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