LINEAR TEMPORAL LOGIC (LTL)

LINEAR TEMPORAL LOGIC (LTL)

Temporal logics (TL)은 다양한 reactive system을 명세하기에 편리한 형식이다. 우리는 이것을 논리적인 시간양식을 시간 추상화 헸다고 말할 수 있다.

linear temporal logic (LTL)는 각각의 지점의 시간 상태에 무한 순서로 이며, linear-time관점에 기반을 둔다. 

Linear temporal property은 사실이되는 무한 시퀀스의 집합을 설명하는 시간적 논리 수식 

그래서 

문제 1

Write the spaceWire spec. in Temporal Logic

ErrorReset

a.

The ErrorReset state shall be entered after a system reset, after link operation is terminated for any reason or if there is an error during link initialization.

ErrorReset상태는 시스템이 리셋된 이후에 입력되어야 한다, link operation이 종료된 이후에 ( 어떠한 이유 or 초기화중 에러)

// 언제 발생해야 하는가?

b. 

in the ErrorReset state the Transmitter and Receiver shall all be reset

ErrorReset 상태에서 송신기와 수신기 모두 다시 설정해야한다. 

// 어떠한 일을 해야 하는가?

c.

when the reset signal is de-asserted the ErrorReset state shall be left unconditionally after a delay of 6,4 us(nominal)and the state machine shall move to the ErrorWait state

// 리셋신호의 주장이 해제될때 6,4us 지연된 후에 조건없이 유지되다 그리고 ErrorWait로 변환될것이다. 

d.

Whenever the reset signal is asserted the state machine shall move immediately to the ErrorRset state and remain there until the reset signal is de-asserted

//리셋신호가 주장 될 때마다, 상태 머신은 즉각적으로 ErrorRset state변환되어야 한다, 그리고 리셋 시그널의 주장이 해제 될때까지 유지 되어여한다.

문제 2

interleaving semantics