HybridSynchAADL: Modeling and Formal Analysis of Virtually Synchronous Cyber-Physical Systems in AADL

Abstract

This thesis presents HybridSynchAADL, techniques for designing and analyzing virtually synchronous cyber-physical systems. Cyber-physical systems (CPSs) are distributed embedded systems that involve both discrete and continuous components. Many CPSs are virtually synchronous; i.e., the implementation is physically distributed, but the logical design behaves synchronously. Virtually synchronous CPSs are used in many areas, including avionics, automotive, robotics, etc. Moreover, these systems are often safety-critical, i.e., malfunctions or errors can lead to enormous damage, even human injuries or deaths. Thus, verification of virtually synchronous CPSs is crucial. Designing and analyzing such systems is difficult due to the combination of distributed characteristics and the continuous dynamics of physical environments. Formal verification can be used to analyze such complex CPSs but there are no sufficient tools and methods to verify virtually synchronous CPSs. We introduce HybridSynchAADL to model and analyze such CPSs. HybridSynchAADL models CPSs using the language that extends AADL. The semantics of HybridSynchAADL is formally specified in rewriting modulo SMT. We have implemented a tool that provides a formal analysis capability based on our semantics. We show the effectiveness of the proposed approach by experimenting the case studies on complex CPSs, such as distributed control of drones.

사이버 물리 시스템 (CPS) 은 분산 네트워크 안에서 연결된 다수의 임베디드 시스템이 연속 동적을 가진 물리 환경과 교류하는 시스템으로 항공, 우주항공, 자동차 등 여러 산업 분야에서 사용된다 . CPS 는 많은 경우 각각의 컴포넌트는 각자의 클럭에 따라 동작하지만, 전체 동작은 어떠한 주기에 의해 동기적으로 동작해야 한다. CPS의 오류나 결함은 금전적, 인적 손해를 입힐 수 있고, 따라서 이를 피하기 위해 개발 단계부터 신뢰할 수 있는 시스템을 설계하는 것이 매우 중요하다.

CPS 를 분석하거나 검증하는 것은 매우 어려운 일이다. AADL (Architecture Analysis & Design Language)은 산업 표준 모델링 언어로 신뢰할 수 있는 시스템을 설계할 수 있도록 지원한다. 하지만 클럭 속도의 오차나 네트워크 지연 시간, 외부 물리 환경과 교류하는 내부 컨트롤러의 샘플링 및 응답 시간의 오차 등과 같은 분산 컴포넌트의 특성과 연속적인 요소를 가진 물리 환경을 모두 고려해야 한다.

CPS 를 분석, 설계하고 검증하는 방법으로는 정형 분석이 사용될 수 있다. 정형 검증은 수학을 기반으로 하여 정형 모델을 생성하고, 이를 통해 시스템의 전체 행동을 탐색할 수 있도록 한다 . 하지만 아직은 분산 및 물리 환경의 특징을 가진 사이버 물리 시스템을 모델링하고 분석할 수 있는 정형 모델링 및 도구는 개발되지 않았다.

이 연구는 물리 환경을 가진 CPS 를 설계하고 분석할 방법을 제안한다. 먼저 CPS 를 모델링 하기 위해 기존 AADL 을 확장하여 연속 동적까지 표현할 수 있는 HybridSynchAADL 언어를 정의하였다. 물리 환경의 상태는 실수 값을 가진 변수로 표현되고, 각 변수의 연속 동적은 연속 함수와 상미분방정식 형태로 나타낸다. 정의한 언어를 통해 물리 환경 뿐만 아니라 , 제어 장치와 물리 환경의 상호 작용을 샘플링 , 응답 시간 및 오차 시간과 같이 여러 타이밍 정보를 통해 나타낼 수 있다 . HybridSynchAADL 의 정형 시맨틱은 rewriting modulo SMT 를 통해 정의하였다. Rewriting modulo SMT 은 rewriting logic 과 SMT 를 결합한 것으로, 외부 물리환경과 상호 작용하는 무한 상태 시스템을 모델링하고 분석할 수 있게 한다. 정의한시맨틱에서 시스템의 상태는 심볼릭 항으로 표현이 되고 , 시스템의 변화는 rewrite rule 과 equation 을 통해 정의한다. 이를 통해 이산적인 제어 장치와 물리 환경의 상호 작용을 정확히 표현할 수 있다. CPS 를 쉽게 모델링하고 분석할 수 있도록, HybridSynchAADL 언어와 정의한 시맨틱을 통합하여 AADL 의 개발 환경인 OSATE 의 플러그인 툴로 개발하였다. 개발한 툴을 통해 주어진 CPS 를 모델링하고, 시스템이 만족해야 하는 요구 사항을 명세할 수 있다 . 툴은 작성된 모델로부터 rewriting modulo SMT 모델을 생성하고, Maude-SMT 를 통해 시스템이 주어진 성질을 만족하는지 분석하여 결과를 보여준다. 제안한 방식의 유용성을 보여주기 위해 분산 드론 시스템에 대한 실험을 진행하였다. 각 드론은 제어 장치를 가지고 있고 , 시간 오차, 네트워크 지연, 계산 시간, 연속 동적으로 인해 비결정적으로 동작한다. 실험은 하나의 경로만 탐색하는 시뮬레이션 실험과 시스템이 주어진 요구 사항을 만족하는지 테스팅과 심볼릭 방식으로 분석하여 비교하였다. 개발한 툴을 통해 분산 드론 시스템이 특정 요구 사항을 만족하는지 검증할 수 있었다.