소프트웨어 오류 자동 검증 기술
두개의 기둥을 갖추어야 소프트웨어 개발 프로세스 소프트웨어 오류 자동 검증 기술 개발팀을 구성하고 운영해야 하는 체계 체계적인 운영을 강제하는 개발 도구 목표의 50%만 달성시켜줌: sw 오류는 계속 나타남 소프트웨어 오류 자동 검증 기술 자동: 소프트웨어가 소프트웨어를 분석 검증: 오류가 없다는 것을 확인해 줌 기술의 성숙도: 무르익어 산업체로 흘러들고 있슴 목표의 나머지 49%를 달성시켜 줄 것임: 무결점 sw
자동검증이 필요한 이유 자동 검증 엄청나게 크고 복잡해 지는 소프트웨어 hw 복잡도 증가속도 << sw 복잡도 증가속도 불가능: 사람이 쉽게 오류를 찾을 수 없슴 저렴한 무결점 sw개발기술 = 자동화된 기술 검증 테스트: 오류 있슴 만 확인 검증: 오류 없음 을 확인 “sw의 벤츠” = sw검증기술로 개발된 제품 = 제품의 품질/명성
성공적인 자동검증 기술들 프로그램 분석(static program analysis) 20-30년 동안 학교에서 무르익은 기술 요약해석(abstract interpretation) 모델검증(model checking) 자동증명(theorem proving) 20-30년 동안 학교에서 무르익은 기술 위의 세가지 기술의 조합이 이제 비로소 실용적인 모습으로 현장으로 퍼지고 있슴
자동검증 기술이 적용된 예(외국) Microsoftware (2001년 이후) device driver sw 검증: SLAM technology 안전한, 오류없는 sw개발에 집중: 요즘 Bill Gates 연설의 기초 Unix/Linux kernel 검증 (2000년 이후) model checking, static analysis 의 조합 os community에서 가장 주목받고 있는 기술: 논문상은 이 분야 AirBus (2002년 이후) aviation controller모듈 sw 검증에 static analysis기술적용 AirBus sw개발 프로세스의 표준으로 static analysis과정을 결정 이기술에 특화된 회사들 등장: AbsInt, PolySpace technologies, Trusted Logic, GrammaTech, Esterel Technologies, Galois Connections, etc.
자동검증 기술이 적용된 예(국내) 예 국내 산업체 적용은 아직 미미 Java, ML 프로그램: 처리되지않는 예외상황으로 프로그램이 갑자기 멈출수 있는가? 검증. C(과학위성1호 OS모듈): 메시지 버퍼 인덱스가 범위를 벋어나지 않는가? 검증. DB프로그램: 열린 테이블이 닫히지 않고 방치되는가? 검증. WEB프로그램(국가보안기술연구소): 웹소스가 알려진 해커의 침입방법에 뚤릴 수 있는가? 검증. 국내 산업체 적용은 아직 미미 AirBus sw subsidiary 아시아 컨설팅 파트너로 논의중: ropas.snu.ac.kr (서울대 프로그래밍 연구실) 프랑스 파트너: Ecole Polytechnique, Ecole Normale Superieure