Reliability of safety critical systems such as nuclear power plants and automobiles has become a significant issue to our society. As more computing systems are utilized in these safety critical systems, there are high demands for verification and validation (V&V) techniques to assure the reliability of such complex computing systems. However, as the complexity of computing systems increases, conventional V&V techniques such as testing and model checking have limitations, since such systems often control highly complex continuous dynamics. To improve the reliability of such systems, statistical model checking (SMC) techniques have been proposed. SMC techniques can check if a target system satisfies given requirements through statistical methods. In this thesis, first, we have emperically evaluated four state-of-the-art SMC techniques in the automobile domain to see the applicability of SMC for assuring the reliability of safety critical systems and compare pros and cons of the four different SMC techniques. Second, we propose a new hybrid SMC technique that integrates sequential probability ratio
test (SPRT) technique and Bayesian interval estimation testing (BIET) technique to achieve precise verification results quickly. In our experiment, the new hybrid SMC was around 4 times faster than BIET. In addition, we demonstrate the effectiveness and efficiency of this hybrid SMC technique by applying the hybrid SMC technique to three safety critical systems in the automobile domain. Finally, as a solution for validating software reliability at an early stage, we propose a methodology utilizing statistical model checking (SMC) techniques. Reliability validation is performed by comparing the allocated reliability goal with the calculated reliability using the probabilities and the relative weight values for the safety functional requirements. By conducting reliability validation early, we can prevent the propagation of the reliability allocation errors and design errors into the later phases. Thereby, we can achieve safer, cheaper, and faster development of safety critical systems.
원자력 발전소나 자동차와 같은 안전필수시스템의 신뢰성은 우리 사회에서 매우 중요한 이슈가 되고 있다. 이런 안전필수시스템에 점점 더 많은 컴퓨팅 시스템들이 이용됨에 따라, 이런 복잡한 컴퓨팅 시스템들의 신뢰성을 보증하는 확인 및 검증 기법들의 수요가 증가하고 있다. 그러나 컴퓨팅 시스템들의 복잡도가 증가함에 따라, 테스팅이나 모델 체킹 등과 같은 기존의 확인 및 검증 기법들은 한계를 가진다. 왜냐하면 이런 시스템들은 종종 매우 복잡한 연속 역학을 제어하기 때문이다. 이런 안전필수시스템들의 신뢰성을 높이기 위해, 통계적 모델 체킹 방법들이 제안되었다. 통계적 모델 체킹 기법들은 주어진 대상 시스템이 주어진 안전 요구사항을 만족하는지를 통계적 기법들로 검사한다. 이 학위 논문에서, 우리는 크게 세 가지의 연구를 수행하였다. 첫째로, 최신의 통계적 모델 체킹 기법 네 가지를 자동차 안전필수시스템에 적용하는 사례연구를 통해 통계적 모델 체킹 기법의 안전필수시스템 신뢰성 보증에 대한 실제적 적용 가능성을 확인하였고 네개의 다른 기법들에 대한 각각의 장단점을 비교 분석하였다. 두 번째로, 우리는 새로운 하이브리드 통계적 모델 체킹 기법을 제안한다. 하이브리드 통계적 모델 체킹 기법은 첫 번째 비교 분석 연구를 통해 알게된 속도가 빠른 기법인 sequential probability ratio test (SPRT) 기법과 정확한 기법인 Bayesian interval estimation testing (BIET) 기법을 통합해 정확한 검증 결과를 빠르게 얻기 위한 기법이다. 우리는 하이브리드 통계적 모델 체킹 기법의 효과 및 효율성을 보이기 위해 우리의 기법을 세개의 자동차 안전필수시스템에 적용했다. 실험결과로부터 우리는 하이브리드 통계적 모델 체킹 기법이 BIET 기법보다 최대 4배 더 빠르고, BIET의 정확도를 유지하며, SPRT보다 정확함을 확인했다. 마지막으로, 소프트웨어 신뢰성을 소프트웨어 개발 프로세스의 이른 단계에서 검증하기 위한 해결방안으로, 통계적 모델 체킹 기법들을 활용해 검증하는 프레임웍을 제안한다. 그리고 제안한 프레임웍을 자동차 안전필수시스템에 적용하는 사례 연구를 통해 실제 안전성 인증을 획득하는 데에 대한 제안한 프레임웍의 적용가능성을 보였다.
