As PLCs are widely used in the digital I&C systems of nuclear power plants (NPPs), the safety of PLC software has become the most important consideration. Software safety is an important property for safety critical systems, especially those in aerospace, satellite and nuclear power plants, whose failure could result in danger to human life, property or environment. It is recently becoming more important due to the increase in the complexity and size of safety critical systems.
This approach proposes a method to perform effective verification activities on the traceability analysis and software design evaluation in the software design phase. In order to perform the traceability analysis between a Software Requirements Specification (SRS) written in a natural language and a Software Design Specification (SDS) written in Function Block Diagram (FBD), this method uses extended-structured decision tables (ESDTs). ESDTs include information related to the traceability analysis from a text-based SRS and a FBD-based SDS, respectively. Through comparing with both ESDTs from a SRS and ESDTs from a SDS, the effective traceability analysis of both a text-based SRS and a FBD-based SDS can be achieved. For the software design evaluation, a model checking which is mainly used to verify PLC programs formally is used in this research. A FBD-style design specification is translated into input languages of the SMV by translation rules and then the FBD-style design specification can be formally analyzed using SMV.
최근 원전의 안전계통은 기존에 사용되고 있던 아날로그 계통 대신 소프트웨어 기반의 디지털 시스템을 사용하고 있다. PLC가 필수안전계통인 디지털 원전계측제어계통에 널리 사용됨에 따라 PLC 소프트웨어의 안전성은 계통 개발에 있어서 가장 중요한 고려사항이 된다. 최근 새로운 디지털 원전계측제어계통의 안전성을 보장하기 위해서 전 단계에서 소프트웨어 확인 및 검증(V&V)이 채택되었다. 소프트웨어 개발의 전 단계에 걸쳐 수행되는 V&V 프로세스의 적절한 구현은 소프트웨어의 안전성이나 질적 측면에서 보증할 수 있다.
본 논문에서는 소프트웨어 설계명세서(SDS)는 IEC 61131-3에 명시된 그래픽 기반의FBD 형태로 소프트웨어 행위부분이 쓰여지고 FBD 형태의 소프트웨어 설계명세서 기반의 원전계측제어계통을 보다 효과적이고 실제적인 검증 방법을 제안한다. 이 방법은 IEEE 1012에 명시된 설계단계의 검증활동 중 traceability analysis와 software design evaluation에 중점을 둔다.
요구사항 단계에서 자연어로 쓰여진 소프트웨어 요구사항 명세서(SRS)와 설계 단계에서 FBD로 쓰여진 소프트웨어 설계 명세서(SDS) 사이에서 traceability analysis를 수행하기 위해서 Extended-Structured Decision Table (ESDT)를 사용한다. 우선 요구사항 단계의 자연어 SRS에서 object를 추출하여 각 object의 속성과 행위를 묘사하는 object diagram으로 나타낸다. 생성된 object diagram을 ESDT로 표현하여 요구사항 단계의 SRS를 분석한다. 다음으로 설계 단계의 FBD 형태의 SDS에서 ESDT로 표현하여 설계 단계의 SDS를 분석한다. 최종적으로 텍스트 기반의 요구사항 단계와 그래픽 기반의 설계 단계에서 생성되는 ESDT들을 비교함으로써 traceability analysis를 수행할 수 있다.
FBD 형태의 설계명세서의 software design evaluation를 효과적으로 수행하기 위해서 모델체킹(model checking)으로 소프트웨어의 안전성을 자동으로 증명한다. 검증 대상 시스템이 만족해야 할 특성들을 CTL로 명세하여 정의된 translation rule에 의하여 변환된 모델입력언어와 함께 SMV도구에 입력하면 SMV의 모델입력언어로 나타내어진 모델이 CTL로 표현된 요구 명세를 만족하는지의 여부를 효율적이고 자동적으로 검사할 수 있다.
원전계측제어계통에서 제안된 검증방법의 사용가능성을 타진하기 위해서 원전계측제어개발사업단(KNICS)에서 현재 개발 중인 Auto Test and Interface Processor(ATIP)와 고리 1호기의 안전계통인 ATWS Mitigation System(AMS)에 적용해보았다. 설계단계에서 생산되는 설계사양서에 임의적으로 faults를 주입하였을 경우, 제안된 방법론을 사용하여 검증을 수행하게 되면 faults를 정확히 찾아낼 수 있었다. 이 적용들을 통하여 제안된 검증방법은 설계 단계에서의 검증뿐만 아니라 나아가서는 FBD에 의한 구현 단계의 검증까지 동시에 이용될 전망이다. 또한 제안된 검증방법은 서로 다른 기반으로 기술된 두 명세서의 비교나 그래픽 기반의 시스템 행위 명세의 정확성과 완전성 검증에도 사용될 수 있을 전망이다.
