| 오늘날 컴퓨터 시스템의 사용은 날로 증가하고 있으며, 우리가 사용하는 컴퓨터 시스템은 점점 더 다양화, 대형화되고 있다. 즉, 일반적으로 사용하는 데스크탑 PC, 노트북용 PC만이 아닌 비행기, 자동차, 의료장비, 발전소 제어 시스템 등에 다양한 컴퓨터 시스템이 탑재되고 있다. 이러한 환경에서는 사소한 하드웨어, 소프트웨어의 오류가 막대한 인명적, 금전적 손실로 이어질 수 있다. Intel Pentium 오류, Arian-5 로켓폭발, Therac-25 방사선 치료기기 오작동 등이 이러한 예라고 할 수 있다. 이러한 예들을 통해서, 기존의 테스팅이나 시뮬레이션 기법을 바탕으로 하는 오류 검사 방법에는 한계가 있음을 알 수 있다. 그리하여, 본 연구실에서는 수학적, 논리적 이론을 바탕으로 컴퓨터 시스템의 모든 상태들을 검사할 수 있는 정형검증 (formal verification) 기법을 연구한다. 즉, 기존의 정형기법 방법들을 보다 발전시킬 수 있는 연구들을 진행하며, 또한, 기존의 정형검증 방법들을 이용하여, 다양한 safety critical system들에 적용하는 연구를 진행한다. | |
| 주요 연구 분야 |
|
|---|