http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
- 中文 을 입력하시려면 zhongwen을 입력하시고 space를누르시면됩니다.
- 北京 을 입력하시려면 beijing을 입력하시고 space를 누르시면 됩니다.
RISS 인기검색어
- 검색키워드
- 주제어 : UPPAAL (검색결과 6 건)
-
UPPAAL을 이용한 AUTOSAR OS기반 응용 프로그램의 schedulability 검증
오늘 날 차량용 전자제어 시스템의 복잡도는 점차 증가하고 있으며 이에 따라 자동차 안전 요구사항과 타이밍에 관한 제약사항들도 증가하고 있다. 현재의 개발 방식에서 타이밍 제약사항에 대한 검증은 주로 구현 단계에서 이루어지고 있다. 개발 완료 단계에서 발견된 설계의 실수는 많은 추가 비용과 시간을 필요로 한다. 이러한 문제를 해결하기 위해 설계 단계에서 시스템의 타이밍 제약사항을 검증하는 연구가 활발히 이루어지고 있다. 본 논문에서는 AUTOSAR OS에서 실행되는 실시간 응용 프로그램에 대한 스케줄 가능성(schedulability)을 분석한다. 이를 위해 AUTOSAR OS의 태스크와 스케줄러, 프로세서의 timed automata 모델을 제시하고, 모델 검사(model checking) 도구인 UPPAAL을 이용하여 스케줄 가능성을 자동화 검증 및 시뮬레이션 한다. AUTOSAR OS는 OSEK/VDX OS를 기반으로 동작하며 timed automata 모델링을 위해 OSEK/VDX OS 표준을 따른다. 제시하는 timed automata 모델은 단일 프로세서, 고정 우선순위 선점형 스케줄러, 고정 릴리즈 오프셋을 가진 주기적 태스크, 혼합 선점형 스케줄링 정책과 자원 공유를 위한 우선순위 상한 프로토콜을 고려하였다. 모델의 간략화와 직관성을 높이기 위해 UPPAAL 4.1에서 지원하는 스톱워치(stop-watch) 기능을 적용하였으며, 검증 결과로 스케줄 가능성 여부와 태스크 당 최악의 응답시간(worst case response time), 반례(counter example)을 얻을 수 있다. 모델 검사에서 발생하는 상태 공간 폭발 문제를 완화하는 수준의 추상화된 모델을 제시한다. 마지막으로 본 논문에서 제시한 모델에 예제 시스템을 적용하여 스케줄 가능성을 분석하고 설명한다.
-
UPPAAL을 이용한 VANET환경에서 안전 메시지 정형검증 방법 연구
임지훈 高麗大學校 融合소프트웨어專門大學院 2015 국내석사
해마다 도로의 차량이 증가함에 따라 교통사고 및 차량 안전에 관련한 지능형 교통 시스템(Intelligent Traffic System, ITS)의 발전이 비약적으로 성장하였다. 본 논문은 지능형 교통 시스템을 지원하는 VANET 환경에서 IEEE 802.11p 기반의 WAVE 통신 시스템 사용을 위한 기존의 IEEE 802.11 표준 통신 프로토콜의 구조 및 동작을 분석하고 VANET 환경을 고려하여 모델링한다. 본 논문의 주요 연구내용은 IEEE 802.11 표준 DCF 방식의 CSMA/CA 프로토콜의 모델링을 분석하여 VANET 환경에 맞춰 수정하고 간소화하여 모델링한다. 그리고 WAVE로 잘 알려진 IEEE 802.11p의 Control Channel(CCH)을 이용하여 차량 안전에 필요한 안전 메시지 전송을 위해 안전 애플리케이션 성능 분석 자료를 토대로 모델링하고 송신 된 메시지가 지정해 놓은 사양에 맞춰 수신이 이뤄지는 것을 확인한다. 또한 기존의 통신 프로토콜의 수정을 표준으로 맞춰가기 위해 수학적 접근 방식을 이용한 정형검증을 한다. 실시간 속성을 표현 할 수 있는 정형 검증 프로그램인 UPPAAL을 사용하여 패킷 전송의 안전성을 검증한다.
-
MDD 기법을 활용한 산업 자동화 응용 자동 생성 프레임워크
산업 자동화 시스템의 응용 분야가 전문화되고 다양해짐에 따라 시스템의 핵심인 제어 응용의 복잡도와 신뢰성 요구 수준은 급격히 높아지고 있다. 이러한 수요를 충족시키기 위해 응용 개발 프로세스에 모델 기반 개발 (MDD: Model-Driven Development) 기법을 적용하는 연구가 활발히 진행되고 있다. 본 논문에서는 산업 자동화 응용 개발 과정에 MDD 기법을 적용함에 있어서 꼭 필요한 요구사항을 정의하고, 이들 요구사항에 기반하여 신뢰성 있는 검증된 산업 자동화 응용을 개발할 수 있는 프레임워크를 제안한다. 본 논문에서 제안하는 프레임워크는 정형 명세 언어인 타임드 오토마타 기반의 모델링 및 검증 툴인 UPPAAL을 통해 검증된 모델을 산업 자동화 응용으로 자동 변환하며 이 과정에서 모델과 생성된 응용의 행동 (behavior)이 동일함을 보장한다. 또한 통합개발환경 형태로 개발하여 UPPAAL 연동을 통한 모델링 및 검증부터 응용 생성과 실행까지 MDD 기법의 전 과정을 하나의 툴에서 제공하도록 하였으며, 범용 하드웨어와 운영체제 기반으로 패러다임이 전환되고 있는 산업 자동화 시스템에 적용할 수 있도록 다양한 플랫폼을 지원할 수 있는 구조를 채택하였다. 마지막으로 개발된 프레임워크의 동작을 보이고 평가하기 위해 예제 시스템으로 신호등 제어 시스템을 정의하였으며 이를 프레임워크를 통해 산업 자동화 응용으로 개발한 후 실제 산업 자동화 시스템 상에서 동작시켜 평가하였다. As industrial automation systems become more specialized and diverse, the complexity and reliability requirements of control applications, which are the core of the system, are rapidly increasing. In order to meet these demands, researches have been actively conducted to apply model-driven development (MDD) techniques to application development processes. In this paper, we define the necessary requirements for applying the MDD method to industrial automation application development process, and propose a framework to develop reliable and proven industrial automation application based on these requirements. The framework proposed in this paper automatically transforms a model verified through UPPAAL, which is modeling and verification tool based on a formal language timed automata, into an industrial automation application. In this process, it is guaranteed that the behaviors of the model and of the generated application are the same. Also, since it was developed in the form of integrated development environment (IDE), the whole process of MDD method from modeling and verification through UPPAAL to application creation and execution is provided by one tool. In addition, The framework has a structure capable of supporting various platforms so that it can be applied to the industrial automation system in which the paradigm is switched based on the general hardware and the operating system. Finally, in this paper, we developed the industrial automation application using the framework and evaluated the application by operating it on the real industrial automation system.
-
UPPAAL을 이용한 심박수 적응 듀얼 챔버 인공심장 박동기 정형 검증
이선영 高麗大學校 融合소프트웨어專門大學院 2014 국내석사
전자기기에서의 소프트웨어 비중과 복잡도가 점점 늘어나고 있다. 이러한 현상의 일환으로 소프트웨어 자체 오류로 인한 문제 사례가 많이 보고되고 있어 소프트웨어적 결함을 개발과정에서 방지하고 품질을 향상 시켜야 한다는 전 세계적 요구가 확산되고 있다. 특히, 소프트웨어적 결함으로 생명이나 재산상의 큰 손실을 유발하는 경우 소프트웨어 품질 향상과 안전성 보장은 절대적 전제조건이 된다. 이를 위해 세계의 여러 나라는 국제 표준을 만들어 준수하고 있다. 이러한 국제 표준에서 안전성을 보장하는 방법으로 정형기법 사용을 명시하고 있다. 본 논문에서는 위의 사례로 정형기법 커뮤니티에서 선정한 문제 중 하나인 인공심장 박동기의 기본 속성을 정형기법 도구를 이용한 모델링 및 검증을 통해 안전성을 확인한다. 현재 가장 많이 사용되고 있는 심박수 적응 듀얼 챔버 인공심장 박동기(rate-adaptive dual chamber pacemaker)를 대상으로 하며, 인공심장 박동기의 기본 사항은 인공심장 박동기 과제를 관리하고 있는 McMaster 대학의 SQRL에서 제공하는 보스턴 과학의 표준 사항을 포함한 관련 의학 정보를 기준으로 한다. 인공심장 박동기는 주입 후 인공심장 박동기에 의해 발생할 수 있는 부작용이 존재한다. 현재 의학계에서는 인공심장 박동기 증후군으로 분류하고 있으며, 증후군의 종류는 운영 모드에 따라 다르게 나타난다. 이는 인공심장 박동기의 안전성에 위반되는 사항이므로, 이를 방지해야만 한다. 따라서 이를 미연에 방지하기 위해 현재 인공심장 박동기에는 제조사 마다 각각의 알고리즘을 선택적으로 사용하고 있다. 본 논문에서는 보스턴 과학의 표준 알고리즘을 바탕으로 인공심장 박동기 모델을 확장하고 인공심장 박동기 증후군의 주원인이 되는 상심실성 빈맥의 검출 모델을 포함하여 알고리즘의 정확성을 확인하고 안전성을 보장한다.
-
-
연관 검색어 추천
이 검색어로 많이 본 자료
활용도 높은 자료
