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

논문 상세정보

SPARK Examiner를 이용해 ANSI-C프로그램의 안전성을 분석하기 위한 C언어의 제약 조건과 변환 방법
(Restrictions and translation rules of ANSI-C language for analyzing integrity of C program using SPARK Examiner)

김진섭   (한국과학기술원 전자전산학과UU0001375  ); 차성덕   (한국과학기술원 전자전산학과UU0001375  );
  • 초록

    일반적으로 C언어는 고신뢰도를 요구하는 소프트웨어에 적합하지 않다고 알려졌음에도 불구하고 적지 않은 수의 안전성이 중요시되는(safety-critical) 시스템들이 C언어로 구현되었거나 C언어를 기반으로 개발되고 있다. 본 연구의 목적은 C언어의 안전한 subset을 정의하고 이 subset 언어로 작성된 프로그램을 SPARK Ada로 변환하여 SPARK의 분석 도구들을 사용해 프로그램의 안전성을 분석하는 데 있다. SPARK은 Ada의 안전한 subset으로 고신뢰도를 요하는 시스템을 구현하는데 성공적으로 사용되어왔다. SPARK으로 변환된 C 프로그램은 SPARK 수준의 안전성을 갖게 되며 SPARK의 분석 도구인 Examiner를 통해 프로그램의 정확성 검증 등의 분석을 할 수 있다. 본 연구에서는 엘리베이터 컨트롤러 사례 연구를 통해 정의한 subset이 현실적인 시스템을 구현하기에 부족하지 않음을 발견하였으며, SPARK Ada로의 변환을 자동화해주는 변환기를 구현하였다.


    The C language is widely adopted for safety-critical systems. However, it is known that the C language is an unsuitable choice for safety-critical system since the C language includes several bad language features such as heavy use of pointers. The aim of this work is to define safe subset of the C language and translate the subset into the SPARK Ada so that we can verify the program's safety using SPARK analysis tools. SPARK is a safe subset of Ada and has been successfully applied to high integrity system development. The C program translated into SPARK has the same integrity level as SPARK, and the program correctness can be verified by using Examiner which is a SPARK analysis tool. An elevator controller case study is presented and is used to demonstrate the potential use of our approach to implement a realistic system. We also developed a translator that automatically translates C code into SPARK in accordance with the translation rules.


  • 주제어

    프로그램 분석 .   프로그램 변환.  

  • 참고문헌 (10)

    1. B. W. Kernighan, D. M. Ritchie. The C Programming Language. Second Edition, Prentice-Hall, Engle-wood, New Jersey, 1988 
    2. John Barnes. 'High Integrity Ada: The Spark Approach'. Addison-Wesley, chap. 13, 1996 
    3. George C. Necula, Scott McPeak, Westley Weimer. 'CCured: Type-Safe Retrofitting of Legacy Code'. Proceedings of Principles of Programming Languages, 2002 
    4. Trevor Jim. 'Cyclone: A Safe Dialect of C', USENIX Annual Technical Conference, Monterey, CA, June 2002 
    5. Bernard Carre; Joanthan Gamsworthy. 'SPARK-An annotated Ada Subset for Safety-Critical Programming'. ACM Annual International Conference on Ada. Proceeding of the conference on TPJ-ADA '90. 329-402, 3- Dec. 1990 
    6. R. Chapman. 'Industrial Experience with SPARK', Praxis Critical System Limited, ACM SIGADA 2000 Conf. 
    7. Les Hatton. 'Safer C : Developing Software for High-integriry and Safety-critical Systems'. McGraw-Hill, 1995 
    8. W. J. Cullyer, S. J. Goodenough, B. A. Wichmann. 'The choice of computer language for use in safety-critical systems'. Software Engineering Journal 6(2):51-58, March 1991 
    9. Roger S. Rivett. 'Emerging Software Best Practice and how to be Compliant'. Proceedings of the 6th International EAEC Congress. July 1997 
    10. D. Evans. 'Static detection of dynamic memory errors.'. Proceedings of ACM SIGPLAN '96. Conf. On PLDI., SIGPLAN Notices, 31(5):44-53, 1996 

 저자의 다른 논문

 활용도 분석

  • 상세보기

    amChart 영역
  • 원문보기

    amChart 영역

원문보기

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

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

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

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

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