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

논문 상세정보

Statchart/ACSR: Statechart와 ACSR을 조합한 정형 명세
Statechart/ACSR: Combining ACSR and Statechart for Formal Specification

황대연    (고려대학교 컴퓨터학과   ); 김진현    (KAIST 전산학과   ); 안영정    (고려대학교 컴퓨터학과   ); 강인혜    (서울시립대학교 기계정보공학과   ); 최진영    (고려대학교 융합전문대학원  );
  • 초록

    실시간 소프트웨어가 프로세스가 되어 운영체제 위에서 실행이 되면 소프트웨어의 기능만을 명세하는 것으로는 소프트웨어의 안전성을 보장할 수 없다. 때문에 소프트웨어가 올라간 플랫폼의 정보를 포함하여 명세하고 자원과 cpu에 대한 스케줄링 알고리즘도 살펴보아야 비로소 실시간 제약 사항을 만족하는지를 확인할 수 있다. UML에 포함되어 있는 Statechart 언어는 소프트웨어의 행위를 표현하기에 적합하지만 프로세스가 되어 스케줄링 되는 것을 표현하는 것에는 많은 제약이 존재 한다. 본 논문에서는 이처럼 Statechart로는 명세하기 어려운 부분인 자원과 통신에 관련된 특정을 ACSR을 통하여 명세하여 보완하고자 한다. 두 가지 정형 언어를 통해 보다 시스템을 정확하게 명세할 수 있는 방법을 제시하고, 이를 위해 두 언어의 연결을 위한 정형적 문법과 의미를 제시한다.


    For Real-time systems, formally specifying the functional behavior of the software and verifying it is not enough to prove that it will meet its real-time requirement. When a software is loaded as a process and gets restriction on resources, the platform information has to be considered together with the software. In this paper we propose a combination of two formal language, Statechart and ACSR to complement each other's weak point and to formally specify software and platform together.


  • 주제어

    정형 기법 .   실시간 시스템 .   플랫폼 기반 모델링.  

  • 참고문헌 (10)

    1. J E Rumbaugh, G Booch, I. Jacobson, The Unified Modelling Language User Guide, 1999. 
    2. D. Harel, Statecharts, "A visual formalism for complex systems," Sci. Comput. Program., vol.8, no.3, pp.231-274, 1987. 
    3. D. Harel and M. Politi. Modeling Reactive Systems With Statecharts, The Statemate Approach, McGraw Hill, 1998. 
    4. I. Lee, P. Br'emond-Gr'egoire, and R. Gerber, "A process algebraic approach to the specification and analysis of resource-bound real-time systems," Proceedings of the IEEE Special Issue on Real-Time Systems, pp.158-171, Jan. 1994. 
    5. Treharne H, Schneider S., Using a Process Algebra to control B OPERATIONS, IFM'99, York, Springer 1999. 
    6. C. Fischer. CSP-OZ, A combination of Object-Z and CSP, Formal Methods for Open Object-Based Distributed Systems, FMOODS'97, pp.423-438, Chapman & Hall, 1997. 
    7. Jinhyun Kim, Inhye Kang, Jin-Young Choi, and Insup Lee, Timed and Resource-oriented Statecharts for Embedded Software, IEEE Transactions on Industrial Informatics, vol.6 Issue.4, pp.568-578, Nov. 2010. 
    8. Michelle L. Crane, Juergen Dinge, UML vs. Classical vs. Rhapsody Statecharts: Not All Models are Created Equal, Proc. 8th International Conf. on Model Driven Engineering Languages and System, Oct. 2005. 
    9. H. Yoo, K. Lee, J. Choi, Process Algebraic Approach to Timing Analysis of Superscalar Processor Programs, Journal of KIISE : Computer Systems and Theory, vol.27, no.2, pp.117-233, Feb. 2000. (in Korean) 
    10. M. Park, K. Bang, J. Choi, J Lee, S. Han, Equivalence Checking for Statechart Specification, Journal of KIISE : Computing Practices, vol.6, no.6, pp.608-619, Dec. 2000. (in Korean) 

 저자의 다른 논문

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

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

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

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

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

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