Extending the HybridSynchAADL Modeling Language and Tool

Abstract

사이버 물리 시스템(CPS)은 컴퓨팅 디바이스들의 집합으로 구성되어 있으며 각각은 다른 디바이스들과 통신하기도 하고, 센서를 통해 물리 세계의 정보를 셈플링하고 응답한다. CPS 는 기차, 항공기, 그리고 로봇과 같은 여러 산업 분야에서 사용되고 있다. 많은 CPS 는 각각 컴포턴트 별로 각자의 클럭에 따라 동작하지만, 전체 동작은 특정 주기에 의해 동기적으로 동작해야 한다. 이러한 CPS 의 결함은 생명과 직결되는 손해를 끼칠 수 있기 때문에 개발 단계부터 신뢰할 수 있는 시스템을 설계해야 한다. 이러한 CPS 를 분석하기 위해 HybridSynchAADL 연구가 최근에 진행되었다. HybridSynchAADL 은 Hybrid PALS 기반으로 모델링 언어, 정형 시멘틱, 그리고 사용자가 사용할 수 있는 분석도구를 제공한다. HybridSynchAADL 모델링 언어는 산업 표준 모델링 언어인 AADL (Architecture Analysis & Design Language)을 확장하여 연속 동작까지 표현할 수 있다. 모델링 언어의 정형 시멘틱을 정의하여 정형 검증을 수행할 수 있도록 하였다. 또한 HybridSynchAADL 도구는 AADL 개발 환경인 OSATE 플러그인 형태로 개발하여 CPS 를 모델링하고, 시스템이 만족해야 하는 요구 상황을 명세하도록 하였다. 하지만, 기존 HybridSynchAADL 모델링 언어는 간단하며 기본적인 CPS 만을 표현하였고, 다양한 CPS 를 표현하기 위해서는 더 확장된 모델링 언어를 제공해야 했다. 기존 HybridSynchAADL 도구는 이러한 확장된 모델링 언어를 지원하지 않았다. 또한, 정형 분석 방법으로 심볼릭한 도달성 분석 방법만을 제안하였고, 이러한 분석 방법은 물리 환경이 복잡한 모델의 경우 검증하는데 많은 시간이 걸리는 단점이 있었다. 검증 과정에서 불필요한 파일이 생성되거나 구체적인 사례 없이 분석 결과만을 제공하기 때문에 사용자가 분석도구를 사용하여 신뢰할 수 있는 모델을 개발하는데 많은 어려움이 있었다. 이 연구는 기존 HybridSynchAADL 을 확장하는 연구로서 HybridSynchAADL 모델링 언어와 도구를 확장하는 방법을 제안한다. 먼저 AADL 구성 요소들 중, 동기적으로 동작할 수 있는 것들을 선정하고, HybridSynchAADL 모델링 언어를 확장할 수 있는 데이터와 서브프로그램 구성요소를 도입했다. 이를 통해 재귀 함수 호출이나 배열 데이터 혹은 구조 데이터 타입을 사용하여 더 복잡한 CPS 모델을 만들 수 있다. 데이터와 서브프로그램 구성요소에 대한 정형 시멘틱을 정의하여 확장된 모델링 언어도 정형 검증이 가능하도록 하였다. 또한 물리 환경을 상미분방정식 형태로 나타내어 사용자가 연속함수로 표현하지 않아도, 각 변수의 연속 동작을 쉽게 표현할 수 있게 하였다. HybridSynchAADL 도구에서 기능적인 부분과 사용자 인터페이스 부분을 개선하여 더 다양한 모델을 다양한 방법으로 효율적으로 분석하고 개선할 수 있도록 하였다. 모델링 언어가 확장되었으므로, 이를 기반으로 설계된 모델이 유효한 HybridSynchAADL 모델인지 문법적으로 확인하는 도구를 개선하였다. 사용자가 만든 모델을 분석하는 두 가지 새로운 정형 분석 방법인 무작위 시뮬레이션 분석 방법과 포트폴리오 분석 방법을 제안하여 모델에 맞게 다양한 정형 분석 방법을 사용할 수 있게 하였다. 분석하는 과정에서 요구사항과 분석 방법을 사용할 때 필요한 정보들을 분리하여 작성할 수 있도록 새로운 대화 상자를 구현하였고, 분석 결과 요구사항에 반례가 존재할 경우, 구체적인 반례를 보여주어 사용자가 모델을 올바르게 수정할 수 있도록 하였다. HybridSynchAADL 의 CPS 분석 효율성을 보여주기 위해, 다른 CPS 분석 도구들과의 비교를 하는 실험과, 새로운 정형 분석 방법의 검증 효율성을 보여주는 실험을 진행하였다. 이를 위해 6 가지 서로 다른 HybridSynchAADL 모델을 만들었으며, 정형 분석 방법의 효율성을 위해서는 이러한 모델을 버그가 있도록 수정하여 실험을 진행하였다. 첫 번째 실험에서 HybridSynchAADL 은 다른 도구들에 비해 효율적으로 CPS 를 분석함을 보여주었다. 두 번째 실험에서는 포트폴리오 분석 방법이 심볼릭한 도달성 분석 방법과 무작위 시뮬레이션 분석 방법의 장점 모두를 포함한다는 것을 보여주었다.

Cyber-physical systems (CPSs) are integrations of computation and physical processes. Many CPSs are safety-critical systems where safety has higher priority than other software design objectives. Many CPSs are also virtually synchronous for which implementation is physically distributed, but the logical design behaves synchronously. The recent research HybridSynchAADL provides the modeling language, formal semantics, and analysis tool for virtually synchronous CPSs. The HybridSynchAADL modeling language models virtually synchronous CPSs by using avionics modeling standard AADL. The HybridSynchAADL tool supports modeling and verifying HybridSynchAADL models inside the OSATE tool environment. However, the HybridSynchAADL modeling language does not support various controller behavior such as data structures or function calls. The HybridSynchAADL tool cannot model, analyze, and correct such HybridSynchAADL models effectively. The experiments in HybridSynhAADL do not show the effectiveness of HybridSynchAADL to analyze virtually synchronous CPSs over other CPS verification tools. In this thesis, we extend the HybridSynchAADL modeling language and tool. We identify AADL constructs which satisfy synchronous design constraints, introduce data and subprogram AADL components, and define their formal representation and semantics. We present ordinary differential equations for continuous behavior. We also enhance the HybridSynchAADL tool’s functionality and user interfaces by implementing new analysis methods such as portfolio analysis and Run Configuration dialogue respectively. We conduct two experiments which compare the HybridSynchAADL’s symbolic reachability analysis with four reachability analysis tools and use portfolio analysis to show the effectiveness of finding bugs.