A Formal Verification Framework using Traceability-based Selective Model Projection for Large-scale Software = 대규모 소프트웨어를 위한 추적성 기반 선택적 모델 투영을 활용한 정형검증 프레임워크

국문 초록 (Abstract)

정형 검증 기법중 하나인 모델체킹은 안전 필수 시스템의 기능 정확성(functional correctness)를 확인하기 위하여 널리 사용되는 기법이다. 모델 체킹을 다루는 연구는 비교적 작은 규모의 소프트웨어를 대상으로 한다. 운영체제와 같이 크고 복잡한 시스템 전체를 모델체킹으로 검증하는 것은 불가능에 가깝다. 일반적으로 모델체킹을 사용하여 규모가 큰 시스템을 검증하고자 할 때는 소프트웨어를 기능이나 모듈 단위로 나눠서 검증을 수행한다. 하지만 단순하게 나눠진 기능이나 모듈을 검증한 결과는 소프트웨어 전체를 실행했을 때 발생할 수 있는 기능적 결함을 찾아내기는 어렵다. 따라서 대규모 소프트웨어를 대상으로 모델체킹을 수행하고자 할 때, 대상을 목적에 맞게 나누는 방식이 가장 중요하다. 본 논문에서는 추적성을 기반으로 검증 목적에 관련되는 소프트웨어의 특정 부분을 체계적으로 찾아낼 수 있는 선택적 모델 투영(Traceability-based Selective Model Projection) 기법과, 그 기법을 활용하여 대규모 소프트웨어의 정형검증을 수행하기 위한 프레임워크를 제안한다. 프레임워크를 사용해 검증을 수행하기 위해서는 소프트웨어 개발산출물 간의 추적성을 확보하는 것이 선행되어야 한다. 확보된 추적성을 바탕으로 소프트웨어를 수평적 관점 및 수직적 관점으로 모델링 및 검증을 수행한다. 수평적 관점은 소프트웨어 전체를 대상으로 넓고 얕은 모델을 생성하기 위한 관점이며, 수직적 관점은 검증 목적에 초점을 맞춰 소프트웨어의 특정 부분을 상세하게 다루기 위한 관점이다. 제안하는 선택적 모델 투영 기법은 수평적 관점으로 생성한 소프트웨어의 모델을 검증 목적에 맞게 시뮬레이션하고, 시뮬레이션 과정에서 활성화되는 영역을 도출하여 모델의 특정 영역을 도출한다. 모델 투영을 통해 도출한 수평적 모델의 특정 부분은 추적성을 활용해 소스코드와의 관계를 분석한다. 도출된 소스코드로부터 수직적 모델을 생성하고 모델 투영 과정에서 사용된 검증 목적을 사용해 수직적 검증을 수행한다. 제안하는 프레임워크를 사용하여 항공용 실시간 운영체제인 Qplus-AIR를 대상으로 정형검증을 수행하였다. 검증을 위하여 Qplus-AIR가 준수하는 ARINC 653-1 표준으로부터 검증 속성을 도출하였으며, 수평적 관점으로 시스템의 모델을 생성하기 위하여 Statemate를 사용하였다. 투영된 수직적 관점의 모델을 검증하기 위하여 3가지 (SPIN, Times, CBMC) 모델체커를 사용하였다. 사례연구를 통해 제안하는 검증 프레임워크가 대규모 소프트웨어를 검증하기에 적합함을 확인하였다. 또한 밝혀낸 Qplus-AIR의 문제점과 이를 해결하기 위한 방법을 개발팀에 보고하여 개선할 수 있도록 하였다.

다국어 초록 (Multilingual Abstract)

Model checking, one of formal verification techniques, is widely accepted as a useful technique to demonstration of functional correctness for software in safety critical systems. Most studies in application of the model checking have handled a relatively small example which has small amount of state space. Large and complex software, such as operating systems, is hardly possible to be verified as a whole, because model checking has limitation about size and complexity of the model. Although it is possible to apply model checking to the software divided into small parts by a function or a module, the simple division is not enough to verify the functional correctness of them working together. Therefore, identifying all parts of software relevant to the verification purpose is important for the verification using model checking. This dissertation suggests a formal verification framework using selective model projection based on traceability to identify specific parts of software with respect to verification purposes. The framework starts with establishing traceability between products of a software development process. Two verification approaches, a horizontal verification and a vertical verification, conduct modeling and verifying the software. The former models and verifies the software in a wide and shallow point of view which covers a wide range of the software but does not include detail information. The latter, on the other hand, models and verifies the software in a narrow and deep point of view which focuses on a specific parts according to a verification purpose. The selective model projection is a technique to identify relevant parts in source code with respect to a verification purpose for the vertical verification. The projection identifies relevant parts through simulating the model for the horizontal verification with a simulation scenario about a verification purpose. Traceability analysis leads to find the parts in source code that corresponds to the projected parts in the model for the horizontal verification. The parts of source code are modeled and verified in the vertical verification. This dissertation shows that a case study about verification of Qplus-AIR, which is a real-time operating system for avionics, demonstrates feasibility of the proposed framework. Verification properties are derived from the standard specification, ARINC 653-1 which Qplus-AIR complies. Modeling and verification of Qplus-AIR for the horizontal verification uses Statemate, and it checks whether the Statemate model satisfies the properties using a model checker and a simulator. Three model checkers, SPIN, Times, CBMC, are selected to verify models for the vertical verification. The result of the case study demonstrated the feasibility of the framework, and the verification found some property violations which were delivered to the development team.

목차 (Table of Contents)

• Ⅰ. Introduction 1
• 1. Challenges in large-scale formal verification 1
• 2. Limitations of current approaches 2
• 3. Research goals and outline 3
• Ⅱ. Background 5
• 1. Model checking 5
• 1.1. Model checking in a nutshell 5
• 1.2. Model abstraction 7
• 1.3. Code slicing 8
• 2. Traceability Analysis 10
• Ⅲ. Traceability-based Selective Model Projection 13
• 1. The Framework 15
• 2. Traceability Analysis 18
• 2.1. A metamodel for traceability 21
• 2.2. Establishing traceability 23
• 2.3. Traceability analysis assistant 23
• 3. Horizontal verification 24
• 3.1. Statemate 27
• 3.2. Horizontal modeling and verification with Statemate 28
• 4. Model projection 31
• 5. Vertical verification 35
• 5.1. SPIN 36
• 5.2. The Times Tool 37
• 5.3. CBMC 38
• Ⅳ. A Case Study 40
• 1. The target system: Qplus-AIR 42
• 2. Traceability analysis 45
• 3. Property specification 48
• 4. Horizontal verification 49
• 5. Projection and Vertical verification 57
• 5.1.Model checking of Intra-partition communication of Qplus-AIR using SPIN 58
• 5.2.Model checking of the scheduler of Qplus-AIR using Times 68
• 5.3.Model checking about partition and process management using CBMC 75
• Ⅴ. Conclusions and Future Work 81
• References 83
• Appendix A. The Statemate model of Qplus-AIR 87
• Appendix B. The PROMELA model of Qplus-AIR 88
• Appendix C. The Times model of Qplus-AIR 98
• Abstract (in Korean) 106