1994년 영국 공군의 헬기가 스코틀랜드에 추락했다. 이 사고로 탑승자 29명 전원이 사망했다. 사고 원인은 엔진제어 소프트웨어의 오류였다. 1996년엔 유럽우주국(ESA)이 쏘아 올린 아리안 5호 로켓이 발사 40초 만에 폭발했다. 아리안 4호기에 사용한 일부 소프트웨어를 5호기에도 그대로 사용했는데, 이때 발생한 수학적 오류를 무시했기 때문이었다. 잘못 만든 소프트웨어가 얼마나 큰 위험을 초래할 수 있는지 단적으로 보여주는 사례다.
안전한 SW 만드는 SW
오류가 났을 때 엄청난 인명·재산피해를 낼 수 있는 소프트웨어를 ‘고안전성 소프트웨어’라고 부른다. 대표적인 예가 지하철이나 열차 운행에 쓰이는 철도소프트웨어다. 열차 간격을 일정하게 유지해 효율을 높이고, 열차에 이상이 있을 때 제동을 거는 역할을 한다. 한 예로 유럽열차운행관리시스템(ERTMS)을 도입한 유럽에선 중앙시스템과 무선통신을 주고받으며 스스로 움직이는 무인열차를 운행하고 있다.
유럽열차운행관리시스템엔 여러 하드웨어와 소프트웨어가 촘촘히 결합돼 있다. 자동운전장치(ATO)는 열차의 출발, 가속, 정차, 출입문 개폐 등을 자동으로 제어한다. 무선통신을 이용해 열차들의 위치를 실시간으로 파악하고 안전운행에 필요한 속도정보를 차량의 컴퓨터에 전송한다. 운행속도가 허용속도를 초과하면 자동으로 열차속도를 줄이는 자동제어장치(ATC), 비상시 열차를 완전히 멈추게 하는 자동정지장치(ATS)도 적용돼 있다.
자동운전에 사용되는 소프트웨어는 절대 에러가 생겨선 안 된다. 그래서 특별히 고안전성응용개발환경(스케이드)이라는 소프트웨어를 이용해 만든다. 스케이드에는 그래픽을 기반으로 한 ‘정형기법’이 적용돼 있어 소프트웨어의 에러를 없앨 수 있다. 정형기법은 자연어로 만들어진 코딩을 수학적인 기호로 바꿔 완전성·정확성·일관성을 증명하고 검증하는 방법이다.
스케이드는 제작단계에서 소프트웨어의 오류를 자동으로 찾아 준다. 이 과정을 ‘디버깅’이라고 한다. 소프트웨어도 사람이 만들다보니 논리에 맞지 않는 오류가 생길 수 있다. 디버깅은 이런 작업오류와 프로그래밍 문법오류를 제거하고, 필요한 코드를 자동으로 생성해준다. 마치 백신프로그램이 컴퓨터에서 바이러스를 잡아낸 뒤 치료까지 해주는 것처럼 자동화돼 있어 편리하다.
프로그램 내 모든 경로를 테스트하는 콘콜릭(Concolic) 소프트웨어를 사용하기도 한다. 소프트웨어가 처할 수 있는 모든 상황을 검토하려면 비용과 시간, 노력이 많이 든다. 콘콜릭은 다양한 상황을 자동으로 만들어 새로 만든 소프트웨어의 안전성을 체계적으로 검사하는 소프트웨어다. 프로그램의 모든 경로가 실행되거나 사용자가 지정한 종료 조건을 만족할 때까지 반복된다.
믿음직한 SW
미국에선 1956년 그랜드캐년 상공에서 항공기 충돌이 일어난 이후, ‘공중충돌방지장치(ACAS)’를 도입했다. 항공기의 속도와 고도를 실시간으로 파악해 자동으로 충돌을 경고하는 소프트웨어다. 항공기 여러 대가 근처에 있을 때, 가속도에 따른 예상위치를 초 단위로 계산해 충돌위험을 알린다. 이 장치도 스케이드를 이용해 만들었다. 원자력발전소는 다른 어느 곳보다 안전이 중요한 곳이다. 원자로 내부의 수소폭발을 방지하기 위해 실시간으로 수소농도를 측정해 대응하는 ‘수소감시시스템 (HMS)’ 역시 스케이드로 만든다. 믿을만한 소프트웨어는, 믿음직한 소프트웨어가 만든다.
