Formal Verification Framework for Cyber-Physical Systems on PALSware

Abstract

Achieving high-level safety guarantees for cyber-physical systems has always been a key challenge, since many of those systems are safety-critical so that their failures in the actual operation may bring catastrophic results. Many cyber-physical systems have real-time and distributed features, which increase the complexity of the system an order of magnitude higher. In order to tame the complexity, a middleware called PALSware has been pro- posed. It provides a logically synchronous environment to the application layer on top of physically asynchronous underlying network and operating systems. The com- plexity of a system can be significantly reduced in a synchronous environment. However, a bug in PALSware may have destructive effects since it exposes every application system to runtime failures. Moreover, finding bugs in PALSware can be very challenging in some cases, for various reasons. To solve this problem, we present VeriPALS, a formally verified C implementation of PALSware together with a verification framework for application systems. Espe- cially, the framework provides an executable model as an efficient random testing tool. As case studies, we developed two application systems, and applied VeriPALS to demonstrate effectiveness of the framework in both testing and formal verification.

사이버 물리 시스템의 안전성을 높이는 일은 항상 중요한 연구 주제가 되어왔다. 그 이유 는 많은 사이버 물리 시스템이 안전 우선 시스템이기 때문인데, 이는 실제 시스템 구동 중에 오류가 발생할 경우 큰 사고로 직결될 수 있음을 의미한다. 더욱이, 사이버 물리 시스템이 가지는 실시간성, 분산성이 시스템의 복잡도를 높여 위험성을 증가시키므로 안전성을 높이는 일은 매우 중요하다. 시스템의 복잡도 문제를 해결하기 위해, PALSware라는 미들웨어가 고안되었다. 이 미들웨어는 비동기식으로 동작하는 네트워크와 운영체제 환경 위에서 가상의 동기식 환 경을 애플리케이션 층에 제공하는 역할을 한다. PALSware를 사용하면 시스템을 동기식 환경에서 디자인할 수 있게 되어, 시스템의 복잡도를 크게 낮추는 것이 가능해진다. 하지만, PALSware에 버그가 있을 경우 그 악영향이 매우 크게 나타날 수 있다. 우선 이 미들웨어를 사용하는 모든 애플리케이션 시스템에 버그가 존재하게 된다. 또한, 미들 웨어의 버그를 찾는 일은 일반 프로그램의 버그를 찾는 것보다 매우 어려운 문제가 될 수 있다. 이 문제를 해결하기 위해, 우리는 VeriPALS라는 프레임워크를 개발하였다. 이 프레 임워크는 수학적으로 엄밀하게 검증한 PALSware의 C 구현체를 포함하고 있어 안전한 시스템 구현을 돕는다. 또한, 애플리케이션 시스템을 Coq 위에서 수학적으로 엄밀히 검증할 수 있는 기능을 지원한다. 더 나아가서, 이 프레임워크는 실행 가능한 모델을 효율적인 랜덤 테스팅 툴로서 제공한다. 우리는 이 프레임워크 위에서 두 종류의 애플리 케이션 시스템을 개발하고 테스팅 및 엄밀 검증하여 이 프레임워크의 유용성을 보였다.