브로셔요약 - 비상용 디젤 발전기 통제 소프트웨어 검증 by MathWorks

제목: 비상용 디젤 발전기 통제 소프트웨어 검증(Verifying High-Integrity Control Software for Mission-Critical Emergency Diesel Generators)

저자: Dr. Jörg Barrho, 독일

문서유형: 소프트웨어 개발 업체 브로셔(총 3페이지), 2012년

 

원자력 발전소의 디젤 발전기 콘트롤 소프트웨어를 개발하는 IEC 60880 기반 프로젝트에서 Polyspace 코드 검증기를 활용한 사례를 소개한 자료

---

백업용 디젤 발전기

• 주 전기 공급원에 정전 발생 시 발전소 오퍼레이터는 백업용 디젤 엔진 발전기에 의존하여 필수 기능(vital functions)이 처리되도록 함
• 아래 그림의 MTU genset은 원자력 발전소 애플리케이션이 요구하는 높은 수준의 안정성(safety) 및 신뢰성(reliability) 표준을 충족시키는 비상용 디젤 발전기이다.
• 발전기의 가용성을 보장하기 위해 이 MTU 디젤 엔진은 높은 무결성(high-integrity)의 통제 소프트웨어를 사용하며, 이 소프트웨어 개발은 IEC 60880 표준을 기반으로 한다.

[원자력 발전소의 비상 파워 생성에 사용되는 MTU mission-critical 디젤 발전셋]

IEC 60880 표준

• IEC 60880는 컴퓨터 기반 기구(instrumentation)나 원자력 발전소 통제 시스템에서 사용되는 소프트웨어를 위한 요구사항을 정의한다(특히 IEC 61226에 정의된 것처럼 안전성 카테고리 A의 기능을 수행하는 소프트웨어).
• 각 나라의 원자력 규제 기관(nuclear regulatory agency)이 이 요구사항에 보완을 가할 수 있으며, 각 기관은 통제 소프트웨어 및 그 개발 프로세스에 대한 독립적인 감사를 수행한다.
• IEC 60880의 14장은 소프트웨어 도구의 적절한 사용에 대하여 다룬다(소프트웨어 개발 프로세스의 무결성을 개선시키는 도구와 소프트웨어 신뢰성을 향상시키는 도구를 포함).
• 도구는 ‘critical’과 ‘noncritical’로 구분된다. Noncritical 도구의 대표적인 예로 워드 프로세서를 들 수 있다. Critical 도구의 예로는 소프트웨어에 결함을 만들어 낼 수도 있는 컴파일러나 또는 소프트웨어에 있는 결함을 놓칠 수 있는 검증 도구(예, C/C++ 언어를 위한 Polyspace Client)가 있다.

Polyspace 코드 검증기(code verifier) 활용

• MTU 디젤 엔진 통제 소프트웨어 개발에서는 특별히 IEC 60880 요구사항을 충족시키기 위한 구조적 개발 프로세스를 확립함
• 이 프로세스의 핵심 부분 중 하나는 언더플로우, 오버플로우, 0으로 나누기(divide-by-zero), 메모리 액세스 에러, 기타 런타임 에러를 식별 및 제거하는데 Polyspace 코드 검증기를 사용하는 것
• Polyspace 코드 검증기는 특정 카테고리의 런타임 에러로부터 자유로운 것으로 증명된 코드를 부각시켜 개발팀이 그 나머지 코드를 검토하는데 집중할 수 있게 해준다. 즉, Polyspace는 코드의 각 항목을 녹색(런타임 에러로부터 자유로움), 빨간색(오류 가능성 있음), 회색(미실행 unreachable), 또는 오렌지색(미입증 unproven)으로 표시하여 그 상태를 나타낸다.
• MTU 개발자(developers)들은 자신의 코드를 버전 통제 시스템에 체크인 하기 전에 Polyspace를 사용하여 런타임 에러가 있는지를 체크함. 이런 비공식적 테스팅은 개발자에게 코드에 대한 즉각적인 피드백을 주어 정식 통합 테스팅(formal integration testing) 전에 남아 있는 이슈들을 해결하도록 돕는다.
• MTU 빌드 엔지니어(build engineers)들도 매일 밤 진행되는 자동화된 빌드 구축 및 테스트 프로세스의 일환으로 Polyspace를 돌리고 그 결과를 통해 개발자의 관심이 더 필요한 코드 부분을 식별한다.
• 알려진 런타임 에러가 있는 코드(즉, 빨간색으로 표시됨)를 개발자가 제출하는 것은 허용되지 않음. 하지만 오렌지색이나 회색으로 표시된 부분이 있는 코드는 해당 부분이 정당화된(즉, 왜 문제가 되지 않는지 타당한 이유가 설명됨) 경우에 제출 가능하다.
• 모든 코드가 버전 콘트롤 시스템으로 통합된 후에는 전체 코드 베이스를 다시 체크하는데 Polyspace가 사용된다. 즉, 공식 검토 팀(A formal review team)이 빨간색, 오렌지색, 회색으로 표시된 각 코드 부분을 체크하고 그 이유가 타당한지를 확인한다.