서지주요정보
Spark examiner를 이용해 ANSI-C 프로그램을 분석하기 위한 변환기 구현 = Implementation of ANSI-C translator for analyzing C program using SPARK examiner
서명 / 저자 Spark examiner를 이용해 ANSI-C 프로그램을 분석하기 위한 변환기 구현 = Implementation of ANSI-C translator for analyzing C program using SPARK examiner / 김진섭.
저자명 김진섭 ; Kim, Jin-Sup
발행사항 [대전 : 한국과학기술원, 2002].
Online Access 원문보기 원문인쇄

소장정보

등록번호

8013574

소장위치/청구기호

학술문화관(문화관) 보존서고

MCS 02052

SMS전송

도서상태

이용가능

대출가능

반납예정일

초록정보

As computers are progressively invading every area of our life, a failure of a computer, electronic or electromechanical system may cause catastrophic injury or death to human beings. The safety critical applications such as aircraft or nuclear power station control system gain more attentions of software safety researchers. Current commercial programming languages cannot ensure that software is error free and consequently suggestions of safer programming languages play an important role in safety critical systems to ensure reliable software behavior. 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 have 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.

서지기타정보

서지기타정보
청구기호 {MCS 02052
형태사항 v, 66 p. : 삽도 ; 26 cm
언어 한국어
일반주기 부록 : A, ANSI-C의 제한 사항 목록. - B, ANSI-C 코드에서 spark 으로의 변환 규칙
저자명의 영문표기 : Jin-Sup Kim
지도교수의 한글표기 : 차성덕
지도교수의 영문표기 : Sung-Deok Cha
학위논문 학위논문(석사) - 한국과학기술원 : 전산학전공,
서지주기 참고문헌 : p. 49-50
주제 소프트웨어 공학
프로그램 분석
ANSI C
안전성 분석
Software Engineering
safety-critical
program analysis
ANSI C
QR CODE qr code