형식적인 수법을 배웠다

형식적인 수법이 실패했어요.

조금 일찍?(2021/03 정도) 형식수법소용없다이라쓸모가 있을 거예요.라 뜨거워서 공부를 해봤어요(1개월 정도 걸렸어요).
DeNA도 입문 뉴스라고 쓴 것 같은데.

AWS 용지 읽어주세요.

워낙 형식적인 수법이 뭔지 몰라서 알기 쉬운 기사는 없을 것 같다."AWS 용지은~"이라는 말이 자주 나오기 때문에 읽어야 한다.
이거 읽을거리로 좋아요.

시스템의 조작을 정의하기 위해서(그래서formal methods)

기존 자산을 최대한 활용하고 싶어서(그래서tla+)

거의 모든 엔지니어가 2주 정도 따라잡았어요

S3 등에서 빈대 발견 돕기

이렇게 배경과 구체적인 예가 얽혀서 재미있네요.

Lamport에서 배우기

형식과 기법의 언어는 여러 가지가 있지만 위에서 언급한 tla+는 쉽게 손에 넣을 수 있을 것 같아서 그렇습니다.
tla+의 개발자, 수학자, 조화상 수상자Leslie Lamport로서 강좌를 필두로 다양한 자원을 수집하기 위해 노력했기 때문에 기본적으로 그것을 참조한다.헬로월드 수업 영상은 유튜브에도 전재돼 조용한 유머 감각이 흥미로운데 꼭 한번 보세요.

tla+의 내용

내용은 별로 언급되지 않았지만 높은 수준에서'thoroughly testable psedo 코드'를 사용했다.기본적으로 공식에서string으로 시스템의 상태를 정의하고'다음 상태'(x의 다음 상태는 x'로 표시)를 상태 이동도로 정의하여 이상한 행동이 있는지 확인한다. 이런 느낌(safety)과 유사하다.

여러 자원 관리자가 트랜잭션할 수 있는 상태 정의

canCommit == \A rm \in RM : rmState[rm] \in {"prepared", "committed"}

이것은 다음과 같은 형식으로render(외관만 보는 문제).
canCommit ==\forall rm\in RM : rmState[rm]\in {"prepared", "committed"}

자원 관리자 상태 이동의 표시

or조건\/=\lor)과 and조건/\=\land)의 조합

Decide(rm)  == \/ /\ rmState[rm] = "prepared"
                  /\ canCommit
                  /\ rmState' = [rmState EXCEPT ![rm] = "committed"

주의 사항

주의 사항

상태 전환의 정의에 따라 도달할 수 있는 상태를 계산하기 때문에 간단한 알고리즘이라도 매우 긴 시간이 필요하다.모형을 살짝 확대(자원 관리자를 3->5)하면 갑자기 2분->5시간이 된다(너무 크게 하면 안 된다).

tex자를 써야 하기 때문에 익숙하지 않으면 피곤할 수 있습니다.

ASCII에서 비슷해 보이는 기호를 대용하는 것도 습관이 되었다(\neq#.

Lamport의 강의 내용

먼저 motivation의 설명부터 TLA+toolbox의 다운로드와 사용 설명,transation commiit 등 간단한 알고리즘의 설치와 정확성을 검증한다.일일이 손을 대지 않으면 이해할 수 없어 애니메이션의 2배에서 5배가 걸렸다.

해보신 소감.

왜 집합과 위상을 배워야 합니까 같은 책을 읽은 후에 수학이 어떻게 세계를 추상화하고 모형화하는지에 대해 흥미를 느꼈기 때문에 시스템이 이렇게 기술할 수 있는 부분은 상당히 흥분되었다.10년 만에 텍스의 지식이 살아있으니 좀 즐겁다.
대규모 개발, SLA가 매우 엄격하다(개발 기간이 길다) 개발 등은 일반적이라고 생각한다.

개인적 요점

주요 모듈을 대상으로 합니다.tla 파일을 만듭니다.

.tla 파일은 시작----- <module_name> -----, 끝부분=========

import을 INSTANCETC!TCConstant로 정의하고 활용

"Download from the webpage"라고 해도 링크가 없지만 URL을 직접 치면 e.g.https://lamport.azurewebsites.net/video/xxxx.tla나 github를 발견할 수 있다.

tex를 설치하는 데 3시간가량 걸렸다.MacTex가 나쁜 짓을 한 것 같아서 TexLive로 해요.

References

Lamport 웹 사이트https://lamport.azurewebsites.net/

VScode의 tla+ 플러그인https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus）

공식 TLA+Toolbox의 편집기가 약해서 도움을 줄 수 있습니다

tla+의 규격을 가득 채운 리포https://github.com/tlaplus/Examples

Youtube의 강의(

AWS용 용지https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）

MacTexhttps://blog.wtsnjp.com/2020/07/07/about-mactex/)

혼자 공부할 때의 리포https://github.com/banbiossa/learning-tlaplus

쓰여 있어서 참고 가치가 없어요.