As Real-Time Embedded Software (RTES) has been rapidly grown in size and complexity, timing behavioral modeling is desirable to manage its complexity and safety. UML behavioral models with MARTE annotations are used to describe timing behaviors and timing characteristics of RTES. Especially, state machine, sequence, and timing diagrams with MARTE annotations are appropriate to understand and analyze timing behaviors of RTES. However, to guarantee software correctness and safety, timing inconsistencies in UML/MARTE should be identified in the design phase of RTES. UML/MARTE timing inconsistencies are related to modeling errors and can be hazards throughout the lifecycle of RTES.
In this thesis, we propose a systematic approach to checking timing consistency of state machine, sequence, and timing diagrams with MARTE annotations for RTES. We first suggest modeling guidelines for state machine, sequence, and timing diagrams with MARTE annotations. To overcome informal semantics of UML/MARTE models, we provide formal definitions of state machine, sequence, and timing diagrams with MARTE annotations. Then we present the timing consistency checking approach that consists of rule-based and model checking-based timing consistency checking. In the rule-based timing consistency checking, we validate well-formedness of UML/MARTE behavioral models in timing aspects. To this end, we define intra-model and inter-model consistency checking rules for UML/MARTE models. In the model checking-based timing consistency checking, we verify whether timing behaviors of sequence and timing diagrams with MARTE annotations are consistent with the timing behaviors of state machine diagrams with MARTE annotations. For this purpose, timed automata models are transformed from state machine diagrams with MARTE annotations. Timing properties to be verified are extracted from sequence and timing diagrams with MARTE annotations. We support an automated timing consistency checking tool UMCA (Uml/Marte timing Consistency Analyzer) for a seamless approach. UMCA has the capabilities such as rule-based timing consistency checking, model transformation, and timing property extraction. Also, we propose a UML/MARTE model-driven development method supporting by the timing consistency checking approach. We utilize the existing TIMES tool that generates BrickOS-based code. However, BrickOS-based code is not suitable for being used in the development of hard real-time critical systems because it does not satisfy hard real-time constraints. To tackle this problem, we propose transformation guidelines for generating platform-based code from BrickOS-based code. The proposed guidelines convert BrickOS-dependent code into platform-based code while utilizing platform-independent code as it is. Using the transformation guidelines and TIMES tool, platform-based code is generated from the state machine diagrams with MARTE annotations that are checked in the timing consistency checking approach.
The effectiveness and the practicality of the proposed approach are validated using two case studies: cruise control system software and guidance and control unit software. The case studies demonstrate that the proposed approach is capable of effectively detecting timing inconsistencies in UML/MARTE models. Also, the case study for cruise control system software shows that the timing consistency checking approach can be used to generate platform-based code.
The contribution of this thesis lies in the suggestion of UML/MARTE modeling guidelines for RTES, an approach to checking timing consistency in UML/MARTE models, and a UML/MARTE-driven development method using the proposed approach. The proposed approach helps software designers specify consistent state machine, sequence and timing diagrams with MARTE annotations in less effort and time. Domain experts agree that the proposed approach is effective in detecting timing inconsistencies of UML/MARTE models for RTES. Moreover, the proposed approach can be used to generate platform-based code with high quality in timing consistency aspects.
실시간 임베디드 소프트웨어가 날이 갈수록 복잡해지고 코드 크기도 커지고 있다. 실시간 임베디드 소프트웨어 복잡도와 안전성을 효과적으로 다루기 위해서는 시간 행위 모델링이 필요하다. UML/MARTE 행위 모델은 실시간 임베디드 소프트웨어의 시간 행위와 시간 속성을 명세할 수 있다. 특히, MARTE 주석을 가진 스테이트 머신 다이어그램, 시퀀스 다이어그램, 타이밍 다이어그램들은 실시간 임베디드 소프트웨어의 시간 행위를 이해하고 분석하는데 유용하다. 그러나 실시간 임베디드 소프트웨어 정확성과 안전성을 보장하기 위해서는 UML/MARTE 모델들에 내재된 시간 비일관성을 실시간 소프트웨어의 설계 단계에서 식별해서 제거해야 한다. UML/MARTE 행위 모델들의 시간 비일관성은 모델링 에러와 관련이 있어서 오류를 가진 코드가 구현 단계에서 생성될 수 있고, 실시간 임베디드 소프트웨어의 개발 주기에서 소프트웨어 안전성을 위협하는 위험 요소가 될 수 있다.
본 학위논문에서는 실시간 임베디드 소프트웨어의 행위를 명세한 MARTE 주석을 가진 스테이트 머신 다이어그램, 시퀀스 다이어그램, 타이밍 다이어그램들의 시간 일관성을 체계적으로 확인하는 검사 기법을 제안한다. 먼저, 소프트웨어 행위 명세를 위한 스테이트 머신 다이어그램, 시퀀스 다이어그램, 타이밍 다이어그램들의 모델링 방안을 제안한다. 제안 모델링 방안에서는 UML/MARTE 모델들의 비정형적 의미체계를 극복하기 위해서 각 다이어그램들을 정형적으로 정의한다. 그 다음, 규칙 기반 시간 일관성 검사와 모델 체킹 기반 시간 일관성 검사로 구성된 시간 일관성 검사 기법을 제안한다. 규칙 기반 시간 일관성 검사에서는 시간 측면에서 UML/MARTE 모델들의 명세를 검사한다. 이를 위해서 모델 내와 모델 간의 일관성 검사 규칙들이 정의된다. 모델 체킹 기반 시간 일관성 검사에서는 시퀀스 다이어그램들과 타이밍 다이어그램들의 시간 행위가 스테이트 머신 다이어그램들의 시간 행위에서 실행 가능한지를 검사한다. 이를 위해서 스테이트 머신 다이어그램들이 타임드 오토마타 모델들로 변환되고, 상태 다이어그램들과 타이밍 다이어그램들로부터 시간 검증 속성들이 추출된다. 제안한 시간 일관성 검사 기법을 지원하기 위해서 시간 일관성 검사 도구인 UMCA (Uml/Marte timing Consistency Analyzer)를 개발하였다. UMCA는 규칙 기반 시간 일관성 검사와 모델 변환, 그리고 시간 속성 추출의 기능들을 지원한다. 또한, 시간 일관성 검사 기법을 확장하여 일관성 검사가 완료된 스테이트 머신 다이어그램들로부터 플랫폼 기반 코드를 생성하는 방법을 제안한다. 플랫폼 기반 코드 생성에서는 BrickOS 기반 코드 생성을 지원하는 TIMES 도구를 활용한다. 하지만, BrickOS 는 엄격한 실시간성을 보장하지 않아서 실시간 제약성이 중요한 임베디드 소프트웨어 개발에 사용하기는 어렵다. 이 문제를 해결하기 위해서 BrickOS 기반 코드에서 플랫폼 기반 코드를 생성하는 변환 가이드라인을 제안한다. 제안 변환 가이드라인은 BrickOS 기반 코드의 플랫폼 독립적인 코드는 그대로 활용하고, BrickOS 의존적인 코드를 플랫폼 기반 코드로 변환한다.
시간 일관성 검사 기법의 유용성과 실용성을 정속 주행 시스템 소프트웨어와 유도조종장치 소프트웨어의 두 가지 사례 연구들을 수행하였다. 사례 연구를 통해서 제안한 시간 일관성 검사 기법이 MARTE 주석을 가진 스테이트 머신 다이어그램, 시퀀스 다이어그램, 타이밍 다이어그램들의 시간 비일관성들을 효과적으로 식별함을 보였다. 또한, 정속 주행 시스템 소프트웨어에 대한 사례 연구에서는 시간 일관성 검사 기법이 플랫폼 기반 코드를 생성하는데 활용할 수 있음을 보였다.
본 학위논문에서는 실시간 임베디드 소프트웨어에 대한 UML/MARTE 모델링 방안과 시간 일관성 검사 기법, 시간 일관성 검사 기법을 이용한 플랫폼 기반 코드 생성 방법들을 제안하고 사례 연구를 통해서 검증하였다. 본 연구의 독창성은 타이밍 다이어그램에 대한 시간 일관성 검사를 수행한 첫 연구라는 점과 시간 일관성 검사를 통한 플랫폼 기반 코드의 생성 방법을 제시한 점에 있다. 제안한 시간 일관성 검사 기법은 소프트웨어 설계자들이 적은 노력과 짧은 시간 안에 일관성 있는 UML/MARTE 모델들을 명세할 수 있게 도와준다. 도메인 전문가들도 제안한 시간 일관성 검사 기법이 실시간 임베디드 소프트웨어 행위를 명세한 UML/MARTE 모델들의 시간 비일관성을 검출하는데 효과적임을 동의하였다. 또한, 제안 기법은 시간 일관성 측면에서 높은 품질을 가진 플랫폼 기반 코드를 생성하는데 사용할 수 있다.
