페이퍼요약 – 자동차 시스템의 피처 지향 요구사항 확인 by Zhou

제목: 자동차 시스템의 피처 지향 요구사항 확인(Towards Feature-Oriented Requirements Validation for Automotive Systems)

저자: Jiale Zhou 외 5인, 스웨덴

문서유형: 페이퍼(총 9페이지), 2014년

 

자동차 분야 시스템의 피처 지향 요구사항 명세를 형식화하여 밸리데이션 하는 방법을 차 잠금(Vehicle Locking-Unlocking) 시스템을 예로 들어 설명한 자료

---

 

피처 모델(Feature models)

• 자동차 산업 분야의 성숙도 및 표준화 정도가 높아지면서 피처 모델이 자동차 시스템의 요구사항 명세에 널리 사용됨
• 피처 모델은 피처(features)들의 집합을 통해 소프트웨어 제품 라인의 공통성(commonality)과 가변성(variability)을 포착함
• 피처는 최종사용자가 이해할 수 있는 논리적 기능 단위(a logical unit of functionality)이며, 피처와 관련된 요구사항(‘피처 요구사항’이라고 칭함)과 그에 상응하는 동작적 명세(‘피처 동작’이라고 칭함)로 구성됨
• 하나의 제품(a product)은 피처 모델로부터 한 무리의 피처(이를 ‘피처셋’이라 칭함)를 선택함으로써 구성될 수 있음. 마찬가지로 피처 모델로부터 다른 피처셋을 선택함으로써 제품 변종(Product variants)이 구성될 수 있다.

 

피처셋의 유효성(validity) 확인

• 피처셋의 유효성(validity)을 구조적(structural)과 기능적(functional) 두 가지 관점에서 볼 수 있음. 구조적 관점은 선정된 피처가 피처 모델이 정의한 제약(constraints)을 준수해야 함을 나타내며, 기능적 관점은 두 개(또는 여러 개)의 피처 동작 명세(feature behavioral specifications)들 간에 바람직하지 않은 동작이 존재하지 않아야 함을 가리킴
• 피처셋의 유효성에 대한 확신을 증대시키기 위해 다양한 피처 지향 요구사항 밸리데이션(feature-oriented requirements validation) 기법들이 개발되었지만 피처 모델의 크기 증가와 피처셋의 가변성이 숨은 결함을 피하기 어렵게 만듬
• 특히 ‘피처 상호작용 문제(두 개 또는 여러 개의 피처들이 예상 못한 동작을 보이는 상황)’는 피처가 단독으로 사용될 때는 발견되기 어렵다. 

 

제안 방법

본 논문은 피처 상호작용 문제를 다루기 위해 피처 지향 요구사항 벨리데이션을 위한 모델 기반 방법을 제안한다(아래 4개 단계로 구성).

①    피처 명세(Feature Specification): 제한된 유스케이스 모델링 방법인 RUCM(the restricted use case modeling approach)*에 따라 피처의 동작과 요구사항을 명세한다.

②    피처 동작 형식화(Feature Behaviors Formalization): eTASM(the extended Timed Abstract State Machine)** 명세 언어를 사용하여 피처 동작을 형식화한다. 즉, RUCM 유스케이스를 실행가능한 형식 모델인 eTASM으로 변환함

③    피처 요구사항 형식화(Feature Requirements Formalization): 밸리데이션을 위해 eTASM에서 Observers 기법을 사용하여 피처 요구사항을 모델화한다.

④    피처 밸리데이션(Feature Validation): 선택된 피처에 있는 숨은 결함을 발견하기 위해 세 종류의 모델 기반 밸리데이션(논리적 일관성 체킹, 커버리지 체킹, 모델 체킹)을 수행한다.

 

*RUCM은 기존 UML 유스케이스 다이어그램을 확장한 유스케이스 모델링 방법으로, 유스케이스 템플리트와 26개의 제한 규칙(모호성을 줄이고 자동화된 분석을 용이하게 하기 위한 목적)을 제안한다.

 

 

**eTASM은 고안전 시스템(safety-critical systems) 명세를 위한 형식 언어(a formal language)로, 광범위한 수학적 훈련 없이도 이해 및 사용 가능한 명세 언어인 TASM(the Timed Abstract State Machine)을 Observer 구문과 Event 구문을 가지고 확장한 것이다.

 

애플리케이션 예: Vehicle Locking-Unlocking(VLU) 시스템

• 제안된 피처 지향 요구사항 밸리데이션 방법을 설명하기 위해 단순화된 자동차 잠금/잠금 해제(Vehicle Locking-Unlocking: VLU) 시스템을 사용
• VLU 시스템은 자동차 접근을 제어하는 기계적 열쇠를 대체하려는 목적이며, 피처 지향 요구사항 명세의 공통 패턴을 따른다. 즉, 기본 기능이 개별 피처로써 인캡슐레이션되고, 추가적/선택적 개선점(증진 기능)도 피처로써 명세된다.
• VLU의 피처로 Central Locking(CL), Auto-lockout(AUL), Anti-lockout(ANL)이 있음. 기본 피처 CL은 사용자 key fob로부터 커맨드를 받으면 차의 모든 문을 잠그거나 또는 잠금 해제한다. 선택 피처 AUL은 차가 멈춘 후 타임아웃이 만료되면 모든 문을 잠근다(운전자가 수동으로 문을 잠그는 것을 잊은 경우 도둑 예방). 선택 피처 ANL은 차가 멈춘 후 키가 시동(ignition)에 있는 동안 문이 잠기지 않게 한다(운전자가 차 밖에 갇히는 것을 예방)

 

[EAST-ADL로 표현된 VLU 시스템 피처 모델]

 

A. 피처 명세(Feature Specification)

시스템의 각 피처를 RUCM 방법에 따라 제한된 자연어로 명세함(아래 두 개의 서브스텝을 수행)

• Step 1.1: 유스케이스 식별(Use Cases Identification): 피처가 한 무리의 응집력 있는 기능들을 요구사항과 동작의 형태로 캡쳐하므로 이 기능들을 분할하고 피처에 대한 전문가의 이해에 기반하여 가능한 유스케이스를 식별함
• Step 1.2: 유스케이스 명세(Use Cases Specification): 제한된 자연어를 사용하여 RUCM 템플리트를 채움으로써 유스케이스가 명세된다. 향후 분석을 용이하게 하기 위해 일부 사전정의된 제한 규칙이 반드시 준수되어야 함

 

 

VLU의 CL 피처에서 아래 표처럼 CL_Lock과 CL_Unlock이라는 두 개의 유스케이스가 식별됨

피처	유스케이스명	피처 요구사항
Central Locking	CL_Lock	시스템이 문을 잠근다.
	CL_Unlock	시스템이 문을 잠금 해제한다.
Auto-lockout	Auto-Lockout	차가 멈추면 20초 후에 시스템이 자동으로 문을 잠근다.
Anti-lockout	Anti-Lockout	키가 시동에 있고 차가 멈추었다면 시스템이 문을 잠금 방지한다.

[식별된 유스케이스와 그에 상응하는 피처 요구사항]

 

CL_Lock과 CL_Unlock의 유스케이스 템플리트가 각각 아래처럼 작성된다.

유스케이스명	CL_Lock
피처 요구사항	시스템이 차의 문을 잠근다.
사전조건	없음
주 액터	Key fob	이차 액터	차 문, 라이트
의존성	없음	일반화	없음
기본 흐름 스텝	1) Key fob가 “lock” 커맨드를 시스템으로 보낸다. 2) 시스템이 문이 닫혀있는지 확인(VALIDATES THAT) 한다. 3) 시스템이 문을 잠근다. 4) 시스템이 잠금 완료를 나타내기 위해 라이트를 깜박거린다. 사후조건: 차 문이 잠김, 라이트가 꺼짐, 시스템이 유휴 상태가 됨
특정 대안 흐름(RFS 기본 흐름 2)	1) 시스템이 아무것도 하지 않는다. 사후조건: 문이 열린 채로 있음, 라이트가 꺼짐
한정된 대안 흐름	없음	글로벌 대안 흐름	없음

[CL 피처의 CL_Lock 유스케이스]

 

유스케이스명	CL_Unlock
피처 요구사항	시스템이 차의 문을 잠금 해제한다.
사전조건	없음
주 액터	Key fob	이차 액터	차 문, 라이트
의존성	없음	일반화	없음
기본 흐름 스텝	1) Key fob가 “unlock” 커맨드를 시스템으로 보낸다. 2) 시스템이 문을 잠금 해제 한다. 3) 시스템이 잠금 해제 완료를 나타내기 위해 라이트를 깜박거린다. 사후조건: 문이 닫혀있지만 잠기지는 않음, 라이트가 꺼짐, 시스템이 유휴 상태
특정 대안 흐름	없음
한정된 대안 흐름	없음	글로벌 대안 흐름	없음

[CL 피처의 CL_Unlock 유스케이스]

 

B. 피처 동작 형식화(Feature Behaviors Formalization)

명세된 RUCM 템플리트를 분석하고 eTASM 모델을 사용하여 상응하는 피처 동작을 정형화함(이 단계는 아래 4개의 서브스텝으로 구성됨)

• Step 2.1 시스템 구성요소 식별(System Constituents Identification): RUCM 유스케이스에서 참조된 관련 시스템 구성요소를 뽑아내고, 이것들을 eTASM 머신으로 명세한다.
• Step 2.2 구성요소 상호작용 식별(Constituents Interaction Identification): RUCM 유스케이스에서 참조된 여러 다른 시스템 구성요소들 간의 상호작용을 식별하고, 이것들을 eTASM 환경 변수로 명세한다.
• Step 2.3 머신 규칙 명세(Machine Rules Specification): 식별된 머신의 가능한 상태들을 분석하고, eTASM 머신 규칙 집합을 사용하여 피처 동작을 명세한다.
• Step 2.4 속성 주석(Property Annotation): 비기능 속성 주석을 관련 eTASM 머신으로 더한다.

 

Step 2.1 시스템 구성요소 식별(System Constituents Identification)

• 유스케이스로부터 외적 구성요소(유스케이스 액터가 시스템과 상호작용하는 외적 구성요소로 간주됨)와 내적 구성요소(각각의 유스케이스가 시스템을 구성하는 내적 구성요소로 간주됨)를 식별한다.
• 외적 구성요소는 실행 시나리오(execution scenarios)를 시뮬레이션 하기 위해 내적 구성요소는 대상 시스템을 시뮬레이션하기 위해 모델화된다.
• VLU 시스템의 식별된 구성요소에 대한 eTASM 머신들의 목록이 아래와 같이 정의됨

 

머신	수량	카테고리	설명
KEY_FOB	1	External	키 fob의 동작을 모델링한다
LIGHT	1	External	라이트의 동작을 모델링한다
DOORS	1	External	차 문의 동작을 모델링한다
IGNITION	1	External	시동(ignition)의 동작을 모델링한다
VEHICLESPEEDSENSOR	1	External	차 속도 센서의 동작을 모델링한다
CL_LOCK	1	Internal	차 문을 잠근다
CL_UNLOCK	1	Internal	차 문을 잠금 해제 한다
AUTO_LOCKOUT	1	Internal	타임아웃이 만료되면 차 문을 잠근다
ANTI_LOCKOUT	1	Internal	키가 시동에 있으면 차 문을 잠금 방지한다

[VLU 시스템을 위해 식별된 eTASM 머신]

 

Step 2.2 구성요소 상호작용 식별(Constituents Interaction Identification)

• 송신 구성요소(즉, 송신자)와 수신 구성요소(즉, 수신자) 간의 두 종류의 상호작용(DTI와 DMI)이 고려됨
• DTI(Data Transmission Interaction)는 데이터(예, 상태 정보, 다양한 센서 값)가 송신자로부터 수신자로 전송되는 것을 표현하며 eTASM 환경 변수로써 모델화된다. DMI(Data Modification Interaction)는 수신자의 데이터가 송신자에 의해 직접적으로 변경됨을 나타내며, 수신자의 환경 변수 값을 직접 변경함으로써 모델화된다.
• 아래 그림은 VLU 시스템에서 식별된 12개 상호작용을 보여줌(실선은 DTI를 점선은 DMI를 나타냄)

 

[VLU 시스템 구성요소들 간의 식별된 상호작용]

 

Step 2.3 머신 규칙 명세(Machine Rules Specification)

유스케이스 흐름에 명세된 문장들에 기반하여 아래 서브스텝을 통해 eTASM 머신 규칙을 명세함

• 구성요소의 가능 상태 식별: 유스케이스 흐름의 형용사와 동사를 분석함으로써 구성 요소의 가능한 상태가 식별될 수 있다. 사용자정의 타입(a user-defined type)이 가능 상태를 표현하기 위해 사용되고, 상태 변수(a state variable)가 구성요소의 현 상태를 나타내기 위해 정의된다.
• 상태의 전이 조건(transition conditions) 식별: 상태 변수의 값과 전이 조건에 따라 특정 머신 규칙의 조건이 주어진다.
• 시스템이 특정 상태에 진입할 때의 액션 식별: 구성요소의 동작과 다음 가능 상태에 기반하여 머신 규칙의 액션이 명세된다.

 

 

VLU 시스템에서는 앞의 표에서 봤듯이 5개의 외적 구성요소와 4개의 내적 구성요소가 고려되며, 외적 구성요소 머신들의 가능 상태가 아래와 같다.

eTASM 머신	가능 상태(possible states)
KEY_FOB	lock, unlock
LIGHT	flashed, off
DOORS	open, close, locked
IGNITION	haskey, nokey
VEHICLESPEEDSENSOR	still, running

 

내적 구성요소 CL_LOCK 머신은 아래처럼 CL_Lock 유스케이스를 모델링한다. 이 머신은 idle과 lockdoor의 두 개 상태를 가지며, Rule ReceiveCommand는 시스템이 key fob로부터 ‘lock’ 커맨드를 수신하는 것을 나타낸다. Rule Locking은 시스템이 문을 잠그는 것을 나타내며, Rule Idle은 머신이 살아 있고 시스템이 idle 상태 임을 나타낸다. (CL_UNLOCK 머신도 이와 유사한 규칙들을 가지지만 자세한 내용은 생략)

[CL_Lock 유스케이스를 모델화한 eTASM 머신]

 

AUTO_LOCKOUT 머신은 Auto-Lockout 유스케이스의 동작을 모델화한다(아래 참조). Rule Timeout은 차가 멈추고 문이 닫혀 있을 때 타임아웃(이 경우 20초) 만료 시 피처가 활성화됨을 나타낸다. Rule Autolock은 시스템이 자동으로 문을 잠그는 것을 나타내며, Rule Timer는 시간 간격을 측정하는 타이머를 나타낸다. Rule TimerReset은 머신을 살아있게 유지하고, 문이 열리거나 차가 주행을 시작할 때 타이머가 리셋 됨을 표현한다.

[Auto-Lockout 유스케이스를 모델화한 eTASM 머신]

 

ANTI_LOCKOUT 머신은 Anti-Lockout 유스케이스에 명세된 동작을 모델링한다(아래 참조). Rule HasKey는 차가 멈출 때 키가 시동에 있으면 피처가 활성화됨을 나타내고, Rule Antilock은 활성화된 후에 시스템이 문을 잠금 해제함을 표현한다. Rule Idle은 머신을 살아있게 유지하고 시스템이 idle임을 나타낸다.

[Anti-Lockout 유스케이스를 모델화한 eTASM 머신]

 

Step 2.4 속성 주석(Property Annotation)

• 비기능 요구사항의 밸리데이션은 대상 시스템의 관련 비기능 속성에 대한 추정치에 기반함
• 비기능 속성의 추정치가 유스케이스에 명세된 비기능 요구사항에 기반하여 결정되거나 또는 기존 시스템의 경험/분석을 통해 결정된다. 예를 들면, WCET(Worst-Case Execution Time) 분석 같은 기존의 잘 알려진 분석 방법을 사용하여 규칙의 지속 시간(time durations)에 대한 추정치를 얻을 수 있음
• 얻어진 추정치는 앞에 나온 eTASM 모델에 주석으로 덧붙여짐. 예를 들어, locking_time과 unlocking_time 같은 주석 용어는 특정 값 또는 값들의 범위를 가짐

 

C. 피처 요구사항 형식화(Feature Requirements Formalization)

eTASM Observer 기법을 사용해 피처 요구사항을 형식화하며 아래의 4개 서브스텝을 거친다.

• Step 3.1 리스너 명세(Listener Specification): 관심 이벤트 시퀀스(시스템의 관측가능한 기능적 동작과 비기능적 속성을 나타냄)와 이 시퀀스가 리스너에 잡혔을 때 오브저버 변수에 취해지는 상응하는 액션을 명세한다.
• Step 3.2 오브저베이션 명세(Observation Specification): 오브저버 변수에 의존하는 프레디켓(predicate)을 형식화한다. Observation의 프레디켓이 참으로 판명되면 피처의 속성이 만족되었음을 의미한다.
• Step 3.3 이벤트 여과(Events Filtering): EventsFilter를 명세함으로써 관심 있는 이벤트를 식별하고 무관한 이벤트는 걸러낸다.
• Step 3.4 추적성 생성(Traceability Creation):  특정 Observer를 텍스트 요구사항으로 연결한다. 이 연결은 커버리지 체킹을 수행하기 위한 요구사항 추적성(형식 언어 요구사항에서 자연어 요구사항으로 추적)에 사용됨

 

VLU 시스템에는 CL_Lock, CL_Unlock, AUL, ANL의 4개의 피처 요구사항이 있음. 아래는 "키가 시동에 있고 차가 멈추었다면 시스템이 문을 잠금 방지한다"라고 기술된 ANL 피처 요구사항의 observer 명세의 예를 보여주며, 관심 이벤트 시퀀스가 세 부분으로 구성된다.

1) "ANTI_LOCKOUTàHaskeyàRuleEnableEvent"는 ANTI_LOCKOUT 머신의 Rule HasKey가 활성화되었을 때 해당 이벤트가 트리거됨을 나타냄(키가 시동에 있는 동작을 모델링)

2) "[ˆ(AUTO_LOCKOUTàAutolockàRuleEnableEvent|CL_LOCKàLockingàRuleEnableEvent)]*"는 AUTO_LOCKOUT 머신의 Rule Autolock이나 또는 CL_LOCK 머신의 Rule Locking을 활성화함으로써 트리거되지 않는 임의의 수의 이벤트를 나타냄(두 규칙 모두 문이 잠긴 동작을 모델링)

3) "ANTI_LOCKOUTàIdleàRuleEnableEvent"는 ANTI_LOCKOUT 머신의 Rule Idle이 활성화되었을 때 트리거되는 이벤트를 나타냄(키가 제거된 상황을 모델링)

 

 

만약 이 이벤트 시퀀스가 탐지되면 Observation "ov == true"가 참으로 판명된다. 이것은 키가 시동에 있으면 키가 제거되기 전에는 문이 잠기지 않는 상황을 나타냄(즉, ANL 피처 요구사항이 eTASM 모델에서 충족됨)

[ANL 피처 요구사항의 Observer]

 

D. 피처 밸리데이션(Feature Validation)

eTASM 모델(형식화된 피처 요구사항)을 기반으로 아래의 분석 스텝을 통해 결함을 찾아냄

• Step 4.1 논리적 일관성 체킹(Logical Consistency Checking): 논리적 일관성은 “명세에 모순이 없음(free of contradictions in the specifications)"을 의미하며, 본 연구에서는 직접 개발한 TASM 툴셋을 사용하여 실행가능한 eTASM 모델 상에서 논리적 일관성 체킹이 수행된다. 비일관성 결함(inconsistency flaws)의 예로 동일한 머신의 두 개 규칙이 동시에 활성화되거나(대개 해당 피처의 명세에 예상치 못한 동작이 있어서 야기됨), 동일한 변수에 다른 머신들에 의한 다른 값들이 동시에 할당되는 경우(대개 해당 피처의 명세에 바람직하지 않은 숨은 피처 상호작용이 있어서 야기됨) 등이 있다.
• Step 4.2 커버리지 체킹(Coverage Checking): 피처 요구사항이 통합된 피처 명세에서 관측될 수 있는지를 체킹하는 것으로, 요구사항 완전성 체킹(completeness checking)의 중요 활동이다. 커버리지 체킹을 수행하기 위해 모든 피처 요구사항이 피처 명세의 실행을 모니터하는 observers로 변환된다(즉, 파생된 eTASM 모델). Observation이 참이 아닌 경우는 피처 명세가 개별 요구사항을 독립적으로는 만족시키지만 통합된 피처 명세에 동작적 불일치가 있음을 의미한다.
• Step 4.3 모델 체킹(Model Checking): eTASM 머신은 기존 연구에서 정의된 전환 규칙을 통해 쉽게 ‘timed automata’로 변환될 수 있으며, 이런 변환은 eTASM 모델의 다양한 속성을 검증하는데 있어 UPPAAL 툴(스웨덴 Uppsala 대학과 덴마크의 Aalborg 대학이 공동 개발한 모델 체커) 사용을 가능하게 한다. 이런 타입의 체킹은 eTASM 모델이 데드락으로부터 자유로운지, 피처 요구사항에 명세된 예상 속성이 eTASM 모델에 의해 충족되는지를 검증하는 것을 목적으로 한다.

 

VLU 시스템 피처의 유효성(validity)을 체크하기 위해 위의 밸리데이션 스텝을 따름. 먼저 형식화된 eTASM 모델상에서 TASM 툴셋을 사용하여 논리적 일관성 체킹을 수행하고 아래와 같은 2개의 불일치를 발견함

• AUTO_LOCKOUT 머신의 Rule Autolock과 ANTI_LOCKOUT 머신의 Rule Antilock이 door_state 변수를 동시에 다른 값으로 업데이트 함. 이 불일치를 분석한 결과, 키가 시동에 있을 때 ANL 피처가 문을 잠금 해제로 유지하는데 그 사이 autolock 타임아웃이 만료되면 AUL 피처가 문을 잠그려 시도함. 선정된 피처들이 이런 상황을 다루기 위한 규칙을 명백히 명세하지 않았기 때문에 바람직하지 않은 동작이 일어남
• CL_LOCK 머신의 Rule Locking과 ANTI_LOCKOUT 머신의 Rule Antilock이 door_state 변수를 동시에 다른 값으로 업데이트 함. 이 불일치를 수정하기 위해 Rule Antilock에게 더 높은 우선순위를 할당하는 방법을 취함(즉, 해당 규칙에 추가적인 조건을 부여). 이는 두 개 규칙이 동시에 활성화되었을 때 Rule Antilock이 먼저 실행되도록 보장한다.

 

앞의 불일치를 제거한 후에는 TASM 툴셋을 적용해 커버리지 체킹을 진행하였고, 모든 eTASM observers의 관측(observations)이 충족됨이 결과로 나옴. 즉, 통합된 피처 명세가 커버리지 체킹 관점에서 피처 요구사항을 충족시킴을 의미함

 

 

모델 체킹을 위해서 eTASM 모델을 timed automata로 전환하고, UPPAAL을 통해 데드락 속성과 피처 요구사항을 체크한 결과 데드락이 없으며 4개의 피처 요구사항(CL_Lock, CL_Unlock, AUL, ANL)이 충족됨을 확인함