대부분의 사람들이 현대 사회의 일상생활에서 소프트웨어가 갖는 막대한 영향력을 인식하지 못한 채 살아가고 있습니다. 우리의 아침을 깨워주는 디지털 자명종 시계, 음식을 빠르게 데워주는 전자레인지, 세탁기, 식기 세척기 등의 생활가전에서 부터 출퇴근 길의 자동차, 교통 신호등, 남녀노소 전국민이 사용한다는 휴대폰, 사무실에서 흔히 보는 컴퓨터와 프린터, 복사기 등등 우리 주변에서 볼 수 있는 모든 전자제품에는 그들을 제어하는 소프트웨어가 장착되어 있습니다.
하드웨어에 있어서 소프트웨어란 인간에게 뇌와 같은 존재로서, 소프트웨어의 오작동은 하드웨어의 오작동의 가장 큰 원인이 될 수 있습니다. 특히, 항공기 조종시스템이나 의료기기, 원자력 발전 제어 시스템 등과 같은 사용자의 생명이나 재산에 엄청난 피해를 입힐 수 있는 시스템을 제어하는 소프트웨어의 오작동은 반드시 사전에 예방해야만 할 것입니다. [소프트웨어 관련 안전 사고 예]
소프트웨어 안전공학의 목적은 복잡하고 다양한 기능을 담당하는 제어 소프트웨어의 작은 오류가 큰 피해를 초래할 수 있음을 인식하고, 소프트웨어 개발의 초기에서 부터 소프트웨어 안전성을 시스템 안전을 위한 필수 분야로 분석하고 검증하여 잠재적인 오류를 사전에 예방하는 것입니다.
우리 연구실은 소프트웨어 안전성 향상 기술을 다음과 같이 크게 세가지의 관점에서 연구하고 있습니다.
Software Requirement Analysis and Verification
소프트웨어 안전성은 시스템이 개발된 이후에 테스팅으로 검증될 수 있는 성질이 아닙니다. (참고 – Shin Yoo: “오류 존재는 보여도 오류 없음을 보일 순 없다“, 사이언스온) 테스팅은 주어진 테스팅 시나리오를 완성된 시스템에 입력하여 시스템의 행위양식이 예상치와 같은 지를 판단하는 기법입니다. 이러한 기법은 “버튼 A 가 눌러지면 문이 열린다” 라는 식의 시스템 행위의 존재를 검증하는 데에는 적합할 수 있으나, “문이 열린 상태에서는 전자레인지는 절대 작동해서는 안된다” 는 식의 행위의 부재는 검증할 수 없습니다. 그러므로, 소프트웨어 안전성 향상을 위한 노력은 시스템이 구상되는 순간에서 부터 소프트웨어 요구사항 정의와 함께 병행되어야 하며, 소프트웨어 초기 설계 단계에서부터 안전성 관련 성질의 검증을 시행하여야 합니다.
소프트웨어 요구사항의 분석과 검증은 요구되는 안전도의 수준에 따라 다음과 같은 세 단계로 나뉘어 진행될 수 있습니다.
1. 정형언어를 이용한 요구 명세서의 작성을 통한 소프트웨어의 기능적, 비기능적 부분의 명확화 [formal specification 의 예]
2. 가시화된 시뮬레이션을 통한 소프트웨어 행위양식의 검증
3. 정형검증을 이용한 안전성 성질의 검증 [일반적인 검증 프로세스]
Model-based Software Development
요구사항 분석단계에서 적용된 안전성 검증기법들은 소프트웨어의 설계의 전과정에 그대로 적용되어야 합니다. 모델기반 소프트웨어 개발 방식은 요구사항에 기초하여 추상적인 모델을 설계하고, 그 모델을 일관성있게 세분화(decomposition, refinement) 하는 과정을 거쳐 최종 프로그램 코드까지 생성해 내는 방식입니다. 이러한 방식은 위에 언급한 세 가지 안전성 분석 기법을 소프트웨어 모델의 세분화를 위한 각 과정에 적용할 수 있는 좋은 토대를 제공하여 초기 모델에서 최종코드까지 일관성 있는 안전성 관리를 가능하게 합니다.
우리 연구실에서는 기존의 모델기반 소프트웨어 개발 도구에 정형적인 안전성 분석기법을 접목하는 방식으로 임베디드 소프트웨어의 안전성 검증에 관한 연구를 수행하고 있습니다.
Software Formal Verification
정형검증 기법은 정형언어로 작성된 요구정의서, 소프트웨어 설계모델, 또는 프로그램 코드 들을 수학적 모델로 변환하여 논리적인 검증을 실시하는 방식입니다. 이러한 방식은 기존의 테스팅에서 주로 다루어온 행위의 적합성 검증 뿐아니라, 높은 안전성을 요구하는 시스템에서 필요로 하는 행위의 부재에 대한 검증도 가능하게 하는 장점을 가지고 있어 항공기 조종 소프트웨어와 같은 safety-critical 시스템에는 필수적으로 적용되는 기법입니다.
우리 연구실에서는 정형검증 프로세스의 자동화에 따른 상태폭발 문제의 해결과 소프트웨어 개발 프로세스와의 효과적인 접목을 위한 연구를 진행하고 있습니다.