Abstract

안전이 필요한 소프트웨어 시스템이 연속적 요구사항을 가질 때에는 검증이 어려웠지만, 최근 국내에서 연속적 요구사항을 이산적 시그널의 집합으로 요약해 모든 경로를 검증하는 검증법이 개발되었다. 안전을 보장하는 검증법은 속도가 장점인 테스팅을 보완할 수 있다.

본문

% 기 - 이러한 시스템이 개발되었다. % 승 - 어려웠던 이유는 무엇인가 % 전 - 어떻게 했는가 % 결 - 이러한 접근법으로 내 문제를 어떻게 접근할까

국내에서 신호시제논리를 이용한 모델검증법이 개발되면서 안전 시스템의 신뢰성을 높이는 데 기여하고 있다. 신호시제논리는 연속적 시스템의 요구사항을 명세하는 논리 체계이며, 모델검증은 이러한 논리를 기반으로 시스템이 주어진 요구사항을 만족하는지 확인하는 기술이다. 소프트웨어가 복잡해지면서 안전성 검증이 중요해지는 시점에 사이버물리시스템, 의료기기, 사물인터넷 등 연속값을 다루면서 안전이 중요한 시스템의 검증이 가능해진다는 건 대단한 희소식이다.

신호시제논리의 검증이 어려웠던 이유는 무한한 상태의 가능성 때문이었다. 예로 ``속도가 100km/h를 넘으면 20초 내에 다시 100km/h 이하로 줄여야 한다.’’ 는 요구조건을 표현하려면 무한한 속도값을 고려해야 한다. 그간 이산적 시스템의 모델 검증은 시스템의 모든 가능한 상태와 경로를 탐색하여 검증하였다. 이는 ``시스템이 항상 안>전 상태를 유지해야 한다" 같이 상태가 유한한 디지털 회로 등에 적합하지, 연속적인 시스템에는 적합하지 않았다.

연구에서는 이를 극복하기 위해 연속적인 상태 변화를 몇 개의 이산적 상수와 강건성 척도(robustness degree)를 가지는 상미분방정식으로 추상화하여 문제를 해결했다. 강건성 척도는 논리식을 참으로 유지하면서 변수 값이 바뀔 수 있는 범위를 말한다. 연구는 연속적 변수에서 논리식 값이 바뀌는 지점의 개수가 제한되어 있을 때, 이산>적 상태 변화로 추상화할 수 있다는 것을 보였다.

모델 검증의 발전은 테스팅을 연구하는 내게 발전의 화두를 던져주고 있다. 모델 검증이 테스팅, 시뮬레이션 기법과 차별화되는 무오류성을 보장함에도, 테스팅과 시뮬레이션 기법은 현장에서 많이 쓰일 것이다. 안전한 결론을 내지 않는 도구인 퍼징, ChatGPT 등이 업계에서 환영받듯이 말이다. 안전성을 보이는 정적 분석과 빠른 동적 분석은 같이 발전하는 것이다. 우리 연구팀은 LLVM을 정적분석해 쓸모없는 코드를 제거 (prune)해 속도의 이득을 이미 본 바 있어, 모델 검증도 연구의 안에 들어올 수 있다는 확신이 든다.