정보과학회 논문지 B : 소프트웨어 및 응용
Current Result Document : 2 / 3
| 한글제목(Korean Title) |
실시간 소프트웨어 모델에서 만족된 속성을 코드에서 확인하는 체계적 기법 및 사례연구 |
| 영문제목(English Title) |
A Systematic Code Verification Approach and a Case Study for the Properties of Real-time Software Model |
| 저자(Author) |
홍광의
지은경
서동원
배두환
Gwangui Hong
Eunkyong Jee
Dongwon Seo
Doohwan Bae
|
| 원문수록처(Citation) |
VOL 40 NO. 12 PP. 0764 ~ 0773 (2013. 12) |
한글내용
(Korean Abstract) |
실시간 시스템을 모델기반 개발 방법론을 적용하여 개발 시, 타임드 오토마타 모델을 만들고 모델 대상으로 정형 검증을 수행한 후, 검증된 모델로부터 코드를 생성할 수 있다. 안전이 보장된 실시간 소프트웨어를 만들기 위해서는 검증된 모델로부터 코드를 생성 시, 모델에서 만족된 속성들이 코드 상에서도 만족되는지 여부를 확인해야 한다. 본 연구는 타임드 오토마타 모델로부터 체계적으로 생성된 코드를 대상으로 모델에서 만족된 속성이 코드에서도 만족되는지 여부를 확인할 수 있는 방법을 제안하고, 심장박동기의 VVI 모드와 DDI 모드 모델에 제안한 기법을 적용함으로 효과성을 보인다.
|
영문내용
(English Abstract) |
Abstract Following the model-driven development method (MDD), real-time software can be developed by building a timed-automata model, verifying the timed-automata model, and generating a code from the verified timed-automata model systematically. In order to make safety assured real-time software, it is necessary to guarantee that the properties satisfied in the timed-automata model are preserved in the code. We suggest a systematic code verification approach where the code is assumed to be generated from the verified timed-automata model systematically. We demonstrate the effectiveness of the proposed approach by conducting a case study of the VVI mode and the DDI mode of the pacemaker.
|
| 키워드(Keyword) |
모델기반 개발 방법론
실시간 소프트웨어
모델검증
타임드 오토마타
model-driven development
real-time software
model checking
timed-automata
|
| 파일첨부 |
PDF 다운로드
|
