Tag Archives: formal verification

상태 분석을 활용한 복잡한 임베디드 시스템에 대한 요구사항 생성하기


Motivation

시스템 엔지니어가 작성한 소프트웨어 요구사항과 소프트웨어 엔지니어가 작성한 코드상의 차이가 크다.

소프트웨어 엔지니어는 요구사항을 코드로 번역하여 시스템 엔지니어가 의도한 시스템의 행동에 부합하다는 기대를 해야만 한다.

해결 방법: State analysis방법을 사용하여 명시적으로 표현한다.

원문 – Generating requirements for complex embedded systems using state analysis

Introduction

State analysis방법론은 다음의 3가지 기본적 원칙을 주장(assert)한다.

  • control은 system operation의 모든 측면을 포함한다. system under control의 모델을 통해 이해될 수 있음
  • system under control의 모델은 명시적으로 식별되고 시스템 엔지니어들 사이의 합의된 것들을 보장하는 방식이어야 함
  • 소프트웨어 설계 및 운영에 영향을 미치는 모델링 방식은 직접적이고 최소한의 번역(translation)을 해야 한다.

State based control architecture

시스템 model을 구현한 소프트웨어는 크게 4가지의 block으로 이루어져 있다.

  • State estimation – System under control에 대해 관찰하고 계측을 통해 시스템의 상태를 예측하는 모듈
  • Hardware Adapter – System under control을 관찰하거나 자극을 주거나 하는 모듈
  • State control – State knowledge를 토대로 시스템의 goal을 달성하기 위해 system under control을 제어하기 위한 방법을 결정하는 모듈
  • State knowledge – State estimation정보로부터 state transition을 시키고 시스템의 상태값을 변경시키는 모듈

 

state based control architecture

State의 정의

시스템의 상태와 그 상태에 대한 우리의 지식이 같은 것이 아니다. 실제로의 상태는 매우 복잡하지만 우리의 인식상에서는 유용한 것들만 추려서 의도에 맞도록 추상화를 시킬 수 있는데, 우리는 이러한 추상화를 “상태 변수”라고 부른다. 시스템의 알려진 상태는 관심 시점(time)에서의 그것의 상태변수의 값이다.

The state of a system and our knowledge of that state are not the same thing. The real state may be arbitrarily complex, but our knowledge of it is generally captured in simpler abstractions that we find useful and sufficient to characterize the system state for our purposes. We call these abstractions “state variables”.
The known state of a system is the value of its state variables at the time of interest.

상태 변수의 사례로는 다음과 같은 것들이 있을 수 있다.

• device operating modes and health;
• resource levels (e.g., propellant; volatile and nonvolatile memory);
• temperatures and pressures;
• environmental states (e.g., motions of celestial bodies and solar flux);
• static states about which we may want to refine our knowledge (e.g., dry mass of a spacecraft);
• parameters (e.g., instrument scale factors and biases, structural alignments, and sensor noise levels); and
• states of data collections, including the conditions under which the data was collected, the subject of the data, or any other information pertinent to decisions about its treatment.

 

Modeling process

  1. Identify needs—define the high-level objectives for controlling the system.
  2. Identify state variables that capture what needs to be controlled to meet the objectives, and define their representation.
  3. Define state models for the identified state variables—these may uncover additional state variables that affect the identified state variables.
  4. Identify measurements needed to estimate the state variables, and define their representation.
  5. Define measurement models for the identified measurements—these may uncover additional state variables.
  6. Identify commands needed to control the state variables, and define their representation.
  7. Define command models for the identified commands—these may uncover additional state variables.
  8. Repeat steps 2–7 on all newly discovered state variables, until every state variable and effect we care about is accounted for.
  9. Return to step 1, this time to identify supporting objectives suggested by affecting states (a process called ‘goal elaboration’, described later), and proceed with additional iterations of the process until the scope of the mission has been covered.

 

Example

논문 참조, skip

 

Control system을 설계하기 위해 모델을 활용하기

Goals

State analysis에서 goal은 time interval에 대한 상태 변수의 값의 기록에 대한 제약사항이다. 좀 쉽게 표현한다면 시스템이 수행되는 동안 반드시 만족되어야 하는 속성 정도로 표현할 수 있겠다. 예를 들면 카메라의 온도가 x와 y온도 사이에 반드시 있어야 한다는 것이 있을 수 있겠다.

Goal은 상태 변수의 값에 대한 이력에 대해 성공/실패를 판정할 수 있는 기준이 될 수 있다. (위의 사례에서 예를 들면 만약 카메라의 온도가 x-10일 경우 (해당 속성이 만족되어야 하는 시점에서) 위의 속성은 시스템에 부합하지 못함을 의미한다.

결국, 이 Goal이라고 하는 것은 model checking에서 검증되어야 하는 시스템에 대한 검증 속성으로도 볼 수 있다. Formal verification이 이렇게 연결이 될 수 있는 것이다. 결국 Goal을 식별한다는 말의 의미는 검증할 시스템이 만족되어야 하는 시스템의 속성을 추출하는 과정이라고 볼 수 있다. 

goal의 사례들

  1. Camera temperature is between 10 and 20 ◦C from 2:00 pm to 3:00 pm (control goal that specifies a constraint on state value, to be maintained by controller).
  2. Camera temperature is transitioning to be between 10 and 20 ◦C by 2:00 pm (transitional control goal that achieves the appropriate precondition for goal #1).
  3. Camera temperature standard deviation is less than 0.5 ◦C from 1:00 pm until 5:00 pm (knowledge goal that specifies a constraint on quality of state knowledge, to be maintained by estimator).
  4. Camera temperature mean value, plus or minus 3-sigma, is in the range 10–20 ◦C [10<= mean −3 sigma <= mean + 3 sigma <=20], from 2:00 pm to 3:00 pm (inseparably-combined control and knowledge goal, specifying constraints on both state value and quality of knowledge).
  5. Camera temperature measurement data collection state contains at least one measurement less than 10s old, from 1:00 pm until 5:00 pm (data goal, specifying a constraint on the state of a data collection).

 

goal의 정교화

시스템의 모델로부터 goal을 100% 추출하는 것은 한계가 있다. 그래서 goal을 정교화하는 작업이 별도로 필요한데, 본 논문에서는 정교화작업을 위한 4개의 규칙을 정의하였다.

  1. A goal on a state variable may elaborate into concurrent control goals on directly affecting state variables.
  2. A control goal on a state variable elaborates to a concurrent knowledge goal on the same state variable (or they may be specified jointly in a single control and knowledge goal).
  3. A knowledge goal on a state variable may elaborate to concurrent knowledge goals on its affecting and affected state variables.
  4. Any goal can elaborate into preceding goals (typically on the same state variable). For example, a “maintenance” goal on a state variable may elaborate to a preceding transitional goal on the same state variable.

 

Goal을 정교화하는 방법의 사례

아래의 예는 1개의 goal로 부터 5개의 추가적인 goal을 식별하는 사례를 나타내주고 있다.

goal elaboration example

결론

  • 시스템 모델을 소프트웨어로 구현하기 위한 architecture framework을 제시함
  • State variable을 활용하여 시스템의 상태를 식별하고, 시스템이 만족해야 하는 속성을 식별함
  • model checking의 본질적인 문제점인 completeness를 보완함
  • Stateflow modeling시에 Modeling 및 model check를 사용하고자 할 때 도움이 될 것으로 기대함
  • 향후 작업으로 Stateflow modeling을 위한 framework를 개발할 때 참조될 수 있을 것으로 기대함
Advertisements

Experience with semi-formal verification(semi-formal verification 경험담)


한글버전은 아래로..

I read the article below and have a look at past experiences.

Http://www.moreagile.net/2016/01/vdd.html (korean version)

When I was studying formal verification at graduate school, I did not have any curriculum in the school. At that time, my major was about testing, so I think it might be very similar, but formal verification was much more academic and noble. And it was much stronger if it could be applied.

It is more powerful because it approaches mathematical proof.
It can also cover parallel systems (not only concurrent systems).

One day, in order to solve the problem of the CAN protocol, there was a research paper about a protocol that prevents the starvation by putting the upper protocol in CAN. I tried the mathematical proof that the starvation do not happen in that protocol. The way I used it was a semi-formal verification .

After using UPPAAL as related tool, I decided to find SMV. (There may be better tools now.)

We modeled the FSM with respect to the MUST protocol, and described the CTL as an attribute that the model should have.

I specified CTL formula which means that  starvation does not occur in that protocol

So I did a couple of tries and done either by modifying the modeling or by modifying the CTL expression.

Then I went to the professor.

“Professor, I did it.”

The reaction was this.

“I know you did it, how can you believe it?”

This is a fundamental problem with model checking.

Can you be confident that you need a review to validate it, and that no matter how strict the review is, the attributes that the model or model should have are fully described?

Can I put my finger? Or can you bet on part of your body?

Honestly, you will not be confident. I did too.

I tried several times and tried to modify the model (debugging) because I felt that the bug model or attribute was perfect before I found the bug, but when I found the counter example in a mathematical proof, … then I am very embarrassed.

“Uh … is this not? … What’s wrong?”

I try to grasp and fix the problem of the model or the property. I think that it is perfect if I do it several times, but it is not that I am confident enough to take my name or honor.

After all, experts have to specify it. But even if it’s an expert, there’s no way to make mistakes …

It was then, but I do not know how it got better now.
At that time, I tried to perform formal verification of the software code, and personally I thought it was inferior, but I do not know if my idea turned out to be wrong. It may be possible because technology is good.

 

 

아래의 article을 읽다가 과거 경험담이 있어서 좀 설명해볼까 한다.

http://www.moreagile.net/2016/01/vdd.html

대학원때 formal verification에 대한 공부를 하다가 학교 내에 교과과정이 없어서 근처 학교에 가서 청강을 1년간 하고 왔었다. 그 당시 본인의 전공은 test에 대한 것이었으니 많이 비슷하다고 생각할 수도 있으나 formal verification이 훨씬 학문스럽고 고상했다. 그리고 적용이 될 수만 있다면 훨씬 강력했다.

  1. 수학적 증명 방식이기 때문에 강력함
  2. parallel system(concurrent system이 아님)에 대해서도 cover할 수 있음.

어느날 CAN 프로토콜이 가진 문제를 해결하기 위해 CAN에 상위 프로토콜을 얹어서 starvation이 발생하는 것을 막아보는 프로토콜에 대한 연구논문이 있었다. 그 프로토콜…지금은 이름도 기억나지 않는 …MUST였던 거 같은데..그 프로토콜에서 추구하고자 하는 starvation이 정말 발생하지 않는지에 대한 수학적 증명을 시도했었는데, 그 때 사용한 방식이 semi-formal verification이었다.

관련 도구로 UPPAAL을 쓰다가, 이것저것 알아보다가 결국은 SMV로 결정했다. (지금은 더 좋은 툴이 있을지도 모른다.)

MUST프로토콜에 대해 FSM으로 모델링을 하고 그 모델이 가져야 하는 속성에 대해서 CTL로 기술을 했다.

CTL식으로 starvation이 일어나지 않는다고 표현했을 것이다. 아마도…

그렇게 해서 몇번의 시도를 하고 모델링을 수정하거나 CTL식을 수정하거나 해서 완료했다.

그리고 교수님께 찾아갔다. 교수님, 다 했어요.

반응은 이랬다.

“네가 했다는 것은 알겠는데, 그것을 어떻게 믿을 수 있지?”

이것이 모델체킹이 가지고 있는 근본적인 문제점이다.

그것을 확인하려면 리뷰가 필요하고, 리뷰를 아무리 엄격하게 한다고 하더라도 그 모델이나 모델이 가져야 하는 속성이 완벽하게 기술되었다고 자신할 수 있을까?

손가락을 걸 수 있는가? 아니면 자신의 신체의 일부를 걸고 베팅할 수 있는가?

솔직히 자신없을 것이다. 나도 그랬다.

몇번 시도하고 모델을 수정하면서(디버깅) 느낀점은, 버그가 생겨난 모델이나 속성이 버그 발견시에는 완벽하다고 느꼈었지만, 수학적 증명 방식으로 counter example을 찾아줄 때, 내가 기대했던 그 counter example이 아니게 될때…그때 엄청 당황하게 된다..

“어..? 이게 아닌가?.. 뭐가 잘못된 것이지?”

찬찬히 뜯어보고 모델이나 속성에 문제가 있음을 파악하고 수정을 한다… 몇번을 하고 나름 완벽하다고 생각하긴 하지만, 그렇다고 나의 이름이나 명예를 걸 만큼 자신있는 건 아니었다.

결국 전문가가 기술해야 하는건데, 전문가라고 해도 실수를 하지 않는다는 법은 없고…

그 당시에는 그랬는데, 지금은 어떻게 더 나아졌는지는 모르겠다.
그 당시에는 소프트웨어 코드에 대해 정형 검증을 하려고 시도했고, 개인적으로는 그것이 부질없다고 생각하고 있었는데, 나의 이런 생각이 잘못된 것으로 판명이 났는지 아닌지는 아직 모르겠다. 기술이 좋아져서 가능하게 될 수도 있을지도 모른다.