페이퍼요약 - 실시간 제약이 있는 고안전 철도 인터로킹 시스템의 검증 by Hartonas-Garmhausen

제목: 실시간 제약이 있는 고안전 철도 인터로킹 시스템의 검증(Verification of a Safety-Critical Railway Interlocking System with Real-time Constraints)

저자: Vicky Hartonas-Garmhausen 외 4인, Carnegie Mellon University, 미국

문서유형: Academic 페이퍼 (총 6페이지) 

철도 인터로킹 시스템의 검증에 정형적 방법(formal method)을 적용하여 테스팅이나 시뮬레이션으로는 찾기 힘든 결함을 구현 전 모델링 단계에서 빠르게 찾을 수 있다는 내용을 기술한 자료

---

정형적 방법(Formal methods)

• 컴퓨터 시스템 검증을 위해 주로 사용되는 방법으로 시뮬레이션과 테스팅이 있지만 현실적으로 완전한 커버리지가 불가능하여 중요한 결함을 놓칠 수 있다는 제약이 있음
• 이를 보완할 수 있는 방안으로 자동으로(automatically) 그리고 완전하게(exhaustively) 시스템의 상태 영역(the state space of the system)을 검색하고 특정 속성(properties)들이 만족되는지 여부를 확인하는 정형적 방법(Formal methods)이 있음. 대개 정형적 검증 도구(formal verification tools)를 사용하여 검증 수행
• 문제점(설계 에러)을 구현 전 개발 초기에 찾아냄으로써 구현 후 디버깅에 들어가는 비용 을 줄일 수 있음

Verus: 정형적 검증 도구

• Verus는 심볼릭 모델 체킹(symbolic model checking)과 정량적 타이밍 분석(quantitative timing analysis)을 제공하는 정형적 검증 도구(a formal verification tool)이다.
• Verus는 C 언어와 유사한 구문(syntax)을 제공하여 시스템의 정형적 명세(the formalization of systems)를 허용한다.
• Verus는 실시간 시스템의 시간 속성을 직접적으로 표현할 수 있는 특별 구문(special constructs)을 제공하며, 심볼릭 모델 체킹과 정량적 알고리즘이 적용될 수 있는 상태 전이 그래프(state-transition graphs)로 컴파일된다.
• 심볼릭 모델 체킹 알고리즘은 상태 영역(the state space)을 완전하게 검색하여 모델이 명세서를 만족하는지 확인한다.
• Verus는 발생 이벤트에 대한 응답 시간(response time to events), 작업 목록 스케쥴(schedulability of a set of tasks), 성능 측정치(performance measures) 같은 정량적 타이밍 정보의 구체적 명세를 허용한다.

ACC 시스템의 정형적 검증

• 본 논문에서는 ACC(Apparato Centrale a Calcolatore의 약자) 시스템의 안전 로직(the safety logic) 검증에 정형적 방법을 적용한 사례를 연구함(적용된 도구는 Verus)
• ACC는 중간 규모 또는 대규모 철도역의 통제를 위해 Ansaldo Transporti에 의해 개발된 높은 복잡도의 고안전(safety-critical) 시스템이다.
• Verus 언어로 ACC 인터로킹 시스템의 정형적 모델(a formal model)을 생성하고, 정성적 속성(예, safety, liveness)과 정량적 속성(예, response times)을 자동으로 분석한다.
• 검증 대상 시스템의 복잡성(모델이 약 10²⁷개의 상태를 가짐)에도 불구하고 단 몇 분만에 분석이 완료됨
• Verus 분석을 통해 시스템 데드록(deadlock)을 유발하는 이상 동작을 발견함

ACC 인터로킹 시스템(Interlocking system) 상세 설명

1) 시스템 아키텍쳐

• 중복(redundancy)에 기반한 바이탈(vital) 아키텍쳐로 구현된 기차역 통제 시스템
• 물리적 장치(레벨 크로싱, 궤도 회선, 신호등, 스위치 등)의 통제를 위해 주변 포스트(peripheral posts)와 중심 기점(a central nucleus)이 연결됨
• 시스템의 중심 기점에 “2-out-of-3” 다수결 로직 구현을 위해 병렬로 연결된 세 개의 독립적인 컴퓨터가 존재. 컴퓨터 각각에서 동일한 애플리케이션 프로그램(각자 독자적으로 개발된 버전)이 돌아가며, 만약 이 중 하나가 불일치하면 vital hardware에 의해 해당 컴퓨터가 제외된다.
• 주변 포스트(The peripheral posts)도 “2-out-of-2” 프로세서 형상의 중복 아키텍쳐(a redundancy architecture)에 기반한다.

2) 검증 이슈

• 통제되는 물리적 사이트(physical plants)의 규모가 큼: 대규모 철도역은 많게는 2000여개의 물리적 장치(physical devices)를 포함하고 있다.
• 불확정성(nondeterminism): 소프트웨어가 확정적(deterministic)이고 가능한 외부 이벤트(예, 작업 요청, 주변 장치의 응답, 주변 장치의 오류)가 완전하게 식별되었다 할지라도 시스템은 언제 다음 리소스가 요청될지 또는 언제 주변 장치에 장애가 발생할지 알 수가 없다. 또한 시스템이 시간적 제약(timing constraints)을 가지므로 응답 시간(response time) 보장이 중요하다.

3) ACC의 안전 로직(The “Safety Logic” of the ACC)

• 물리적 장치의 안전한 운영(the safe operation)을 통제하는 소프트웨어 서브시스템. 외부 오퍼레이터가 요청하는 논리적 기능(the logical functions)을 구현한 서브시스템으로 상위 레벨 아키텍쳐는 아래 그림과 같다.
• 철도역 주변 장치(the peripheral devices) 및 외부 오퍼레이터와 인터페이스되는 이 안전 로직(SL)은 불확정적인 환경에 놓여진 확정적인 반응성 컨트롤러(a deterministic reactive controller)라고 볼 수 있다.
• 외부 오퍼레이터의 수동 커맨드(manual commands)나 주변 장치의 센서가 읽어 들인 정보가 SL의 입력 데이터가 된다. 외부 오퍼레이터는 “레벨 크로싱 1을 오픈”, “트랙 2에서 트랙 5로 루트 설정” 등과 같은 커맨드를 줄 수 있다. 물리적인 장치의 센서는 “레벨 크로싱 1이 오픈되어 있음”, “스위치 2가 정상 위치에 있음” 등과 같은 정보를 보고한다.
• SL의 출력은 “스위치 12를 정상 위치로 이동한다”, “레벨 크로싱 3을 닫는다” 등과 같은 물리적 장치의 통제이며, 애플리케이션 프로세스의 활성화(the activation)를 통제하는 스케쥴러에 의해 통제가 이루어진다.
• 스케쥴러는 프로세스를 그 실행 상태에 따라 활성화시키고(activate), 중단시키고(suspend), 종료시키는(terminate) 순환식 프로그램(a cyclic program)이다. 시스템 전체에 대해 하나의 스케쥴러가 사용된다.

[ACC 안전성 로직]

4) 안전 로직(SL) 명세 내용

• 프로세스 동작(어떻게 프로세스가 다른 프로세스들과 커뮤니케이션 하는지, 변수에 접근하거나 수정하는지, 예외상황에 반응하는지 등등)이 명세서에 정의된다.
• 각 프로세스는 물리적 장치의 형상을 반영하는 상태 변수(a set of state variables)들과 관련된다. 상태 변수(State variables)들은 프로세스 처리(the process computation)의 상태를 나타내는 논리 변수(logical variables)와 센서가 읽어 들인 주변 장치(the peripheral devices)의 상태를 나타내는 통제 변수(control variables)로 구분된다.
• 프로세스는 오퍼레이션의 실행 중에 논리 변수의 값을 변경할 수 있지만 통제 변수의 값을 수정할 수는 없다. 통제 변수 값은 매 주기의(cycle) 초반에 설정 되고 다음 주기 까지는 변경되지 않는다.
• 한 프로세스가 다른 프로세스에게 물리적 장치 커맨드와 자동 커맨드를 내릴 수 있다.
• 프로세스들은 종종 계층 구조(루트를 설정하는 한 프로세스가 물리적 장치를 통제하는 하위 프로세스들을 통제)로 조직된다.
• SL은 단일 쓰레드 처리(single-thread computation) 방식이다. 즉, 특정 순간에 많아야 하나의 프로세스가 활성화되어 있다.
• 프로세스들은 주인-노예 방식(a master-slave way)으로 활성화된다. 스케쥴러가 프로세스에게 컨트롤을 넘기고 프로세스가 컨트롤을 반환할 때까지 자신의 실행을 정지한다.
• 전역 변수(Global variables)들은 프로세스 처리 상태(the status of the computation)를 추적하고 프로세스의 실행을 통제하는 역할을 한다.

5) SL 오퍼레이션에 대한 설명

• 시스템 동작은 오퍼레이션(프로세스에 의해 수행되는 기본 액션들의 집합)에 의해 정의된다. 오퍼레이션에 포함되는 액션으로 변수 값 테스팅, 논리 변수에 값 할당, 주변 장치에 커맨드 전송, 타 프로세스에 자동 커맨드 전송 등이 있다.
• 활성화 테이블(An activation table)에서 오퍼레이션은 프로세스의 활성화를 결정하는 각 이벤트에 연결된다.
• 오퍼레이션은 해당 오퍼레이션을 활성화시키는 이벤트에 따라 성격이 결정된다. 수동 오퍼레이션(manual operations)은 수동 커맨드(manual commands)에 매핑되며, 상태 오퍼레이션(state operations)은 프로세스 상태에 매핑되고, 자동 오퍼레이션(automatic operations)은 자동 커맨드(automatic commands)에 매핑된다.
• 스케쥴러는 한 사이클의 여러 단계(phases)에 있는 여러 종류(예, manual, automatic, state)의 오퍼레이션을 실행한다.
• 명세서는 오퍼레이션 실행 후 프로세스가 무엇을 해야 하는지도 명세한다. 프로세스는 활성화를 종료하거나, 휴식 상태(a resting state)에 들어가거나, 또 다른 오퍼레이션을 실행하여 현재 활동을 지속하거나, 다음 사이클까지 자신의 실행을 정지하거나 할 수 있다. 마지막의 경우 스케쥴러가 다음 사이클에서 해당 프로세스를 재활성화 시킨다. 스케줄러는 두 개의 큐(queues)를 사용하여 현재 사이클과 다음 사이클에서 재활성화 될 프로세스들을 저장한다.

SL의 정형적 모델(the formal model)

• ACC 시스템 안전 로직(SL)의 두 개 프로세스 형상을 검증. 레벨 크로싱의 안전한 운영을 통제하는 시스템(1개의 스케쥴러, LC와 SHUNT의 2개 프로세스, 17개 이상의 오퍼레이션, 물리적 레벨 크로싱의 18개의 다른 형상으로 구성)을 Verus 언어를 이용해 모델링함.
• Verus 모델은 반복적으로 외부 환경으로부터 입력 데이터를 받고, 로직을 평가하고, 프로세스를 활성화하는 SL의 주기적 구조(the cyclic structure)를 표현해 낸다(SL의 메인 루프는 무한 while 구문을 사용하여 구현).
• 불확정성(nondeterminism)을 지원하는 Verus는 불완전한 명세(partial specifications)를 허용한다.
• 아래 Versus 코드는 수동 커맨드 ‘CLOSE_GATE:’에 매핑되는 SL의 수동 오퍼레이션을 구현한 정형적 모델의 일부분이다.

...

if (MAN_cmd == CLOSE_GATE) {

if (CMD_state != MANUAL){

CMD_state = MANUAL;

LC_state = REQUESTED-CLOSING;

}

}

wait(1);

...

SL의 정형적 검증(The formal verification of the safety logic)

• Verus 도구의 심볼릭 모델 체킹 알고리즘을 활용하여 ACC의 안전 로직 서브시스템(SL)을 검증. 상태 전이 관계(The transition relation)는 부울식(boolean formulas)으로 표현되고 이진 의사결정 다이어그램(binary decision diagrams)으로 구현된다.
• Verus를 이용하여 타이밍 요구사항(timing requirements)도 모델링하고 검증한다. Verus는 CTL 식으로 표현된 시간 제약이 없는 속성(untimed properties)의 검증과 RTCTL(real-time CTL) 식으로 표현된 시간 제약이 있는 속성(timed properties)의 검증을 허용한다.
• CTL 식(CTL formulas)은 “p가 결국 발생할 것이다”, “p는 절대 선언되지 않는다” 등과 같은 속성의 검증이 가능하지만, “p가 10ms 이내에 발생할 것이다” 같은 시간 제약적인 속성을 직접적으로 표현하지 못한다. RTCTL 모델 체킹은 모든 CTL 오퍼레이터에 시간 한도(time bounds)를 도입해 이를 보완한다.

1) 안전성 속성(safety properties) 검증

아래 세 가지의 안전성 속성(safety properties)을 CTL 불변식(invariants)으로 표현하고 검증했을 때 단 몇 초 만에 이들이 모두 참(true)임이 확인되었다.

①     레벨 크로싱이 닫히지 않은 경우에는 SHUNT 프로세스가 CLEAR-SIGNAL을 발행하지 않는다.

②       신호등에 CLEAR-SIGNAL이 일단 발행되었다면 레벨 크로싱을 닫는 컨트롤을 잃게 되면서 CLEAR-SIGNAL 발행이 멈춰진다.

③       안전 로직(The Safety Logic)은 한 사이클 내에서 절대 같은 커맨드를 두 번 발행하거나 또는 상충하는(contradictory) 커맨드를 발행하거나 하지 않는다.

2) 데드락(deadlocks) 존재 및 사이클의 종료 여부 검증

• 같은 사이클에서 프로세스가 한 오퍼레이션의 실행을 끝내고 또 다른 오퍼레이션을 계속하는 순환(recursion)이 항상 종료가 되는지 확인 필요. 검증을 위해 이 요구사항을 하나의 속성(a property)으로 모델링함
• 모델 분석 과정에서 데드락이 발견됨. 프로세스가 사이클의 상태 단계(the state phase)에서 런(running)되는 동안에 프로세스의 휴식(RESTING) 상태가 활성화되어 발생되는 루프(the loop)가 있다는 반례(counterexample)를 Verus 도구가 생성해냄
• 명세서에 RESTING 상태에 매핑되는 상태 오퍼레이션(state operations)이 포함되지 않았었음. 이 문제는 휴식 상태(the resting state)와 관련된 null 오퍼레이션(단순히 프로세스를 종료시키는 역할)을 정의함으로써 해결됨
• 정형적 검증에서 발견된 이 루프는 긴 일련의 이벤트가 실행된 후에야 발생하므로 시뮬레이션이나 다른 검증 방법으로 이 문제를 재현해 내기가 쉽지 않다(해당 반례의 깊이가 58-steps으로 시스템의 다양한 요소들간의 복잡한 인터액션에 의해 나타나는 문제임).