Project

[RAFT] RAFT consensus algorithm specification

중간고사가 끝난 이후부터는 RAFT 알고리즘을 maude를 사용해 formal modeling을 진행할 것입니다. 그에 앞서 어떠한 specification을 모델링할지 결정해야 합니다. 따라서, 이 글에서는 RAFT consensus algorithm에 대해 간단히 소개하고 modeling하고자 하는 specification을 작성하고자 합니다. RAFT consensus algorithm RAFT consensus algorithm은 모든 node가 동일한 상태를 유지하며, tolerance를 보장하기 위해 고안된 알고리즘이다. 때문에 일부 node에 문제가 생겨도 전체 system이 잘 동작해야만 한다. 구성 모든 node는 아래 3가지 상태 중 한 가지를 가진다. cluster란 여러 subsys..

[Maude] Token Ring 검증

이 글에서는 Designing Reliables Distributes Systems, 225p에 있는 Token Ring을 maude를 사용해 formal modeling하고 원하는 검증을 진행합니다. 원 프로젝트는 RAFT consensus algorithm을 모델링하는 것이지만, 그 전에 손풀기 느낌으로 좀 더 쉬운 token ring을 모델링합니다. Token Ring In the “token ring” mutual exclusion algorithm, the nodes logically form a “ring” structure, as shown in Figure 13.1 where a node only knows the next node in this ring. The algorithm work..

[Model Checking] Designing Reliable Distributed Systems

TODO Ch. 2 : 자연수, 정수, list, binary tree, multiset 등 data type 정의 Ch. 3 : equational specification이 만족하는지 확인 Ch. 8 : rewrite logic을 사용해서 concurrent behavior 작성 방법을 설명 Ch. 9 : rewriting logic을 사용해서 system의 동작 하나를 분석하는 방법 FREE Ch. 10 : concurrent Ch. 11 : communication Ch. 12 : TCP와 같은 transport protocol 모델링 Ch. 13 : distributed DB 모델링 Ch. 2 Data Types Module fmod MODULE_NAME is MODULE_BODY endfm o..

[Model Checking] 과제연구 주제 정리

지도교수님과 여러 가지 이야기를 나눴고, [특정 모델 체킹 언어를 사용해, 특정 시스템의 모델 체킹을 해 보기]를 주제로 과제연구를 진행하기로 했다. 대충 flow는 아래와 같다. 특정한 model checking 언어를 공부한다. 어떤 system을 체킹할 지 확인하기 distributed key-value store (cloud DB) RAFT consensus algorithm 위 2개를 추천받았는데, 모델링하기 위해서는 해당 system의 동작 방식을 알아야 한다. 일단 백엔드로 갈 거니까 분산 DB를 공부하는 게 좋아보인다. safety, fairness 등 어떤 property를 모델링할지 결정하기 Model Checking 언어 공부 model checking tool은 몇 가지가 있는데, ..

[Model Checking] Linear Time Properties

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. model checking의 주된 알고리즘은 transition system과 requirement를 model checker에 넣어, 해당 transition system이 requirement를 만족하는지 여부를 확인하는 방법이다. 그래서 지금까지 transition system을 모델링하는 방법을 살펴봤었고, 지금부터는 requirement를 모델링하는 방법을 살펴볼 것이다. 이 포스트에서는 크게 4가지를 살핀다. state-based and linear t..

[Model Checking] Modeling Concurrent System

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. 지난 글에서는 Transition System과 Program Graph, 그리고 Program Graph를 Transition System으로 변환하는 방법을 살펴 봤다. 여기서 살폈었던 것들은 닫힌 계로써, 단 하나의 프로그램만 모델링하는 방법이었다. 이제 총 n개의 parallel system P$_1$, P$_2$, ... P$_n$ 이 있을 때를 모델링하고자 한다. 이 때 각 thread의 행동은 아래 3가지 중 하나이다. no communication ..

[Model Checking] Transition System과 Program Graph

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다. 이 글에서는 model checking에서 사용하는 transition system이 대체 뭔지, 그리고 우리가 사용하는 일반적인 프로그램을 transition system으로 바꾸는 방법을 살펴본다. Transition System transition system은 directed graph로 나타낸다. 이 때 graph의 node는 state를, edge는 transition을 의미한다. Definition. Transition System transition..

[N2T] 리팩토링 기록

리팩토링 하게 된 계기 개발 동기 Naver2Tistory는 사실 내가 사용하기 위해 만든 프로그램이다. 2022년 10월쯤에 개발 블로그를 네이버에서 티스토리로 옮기기로 결정하면서 안에 있는 포스팅들을 다 가져오고 싶었는데, 그동안 작성했던 포스팅이 약 300개 가량 되다 보니 수작업으로 일일히 옮길 수 없었다. 이를 위해 Naver2Tistory를 당시 내가 구현할 수 있는 수준으로 만들었었다. 만들다 보니 블로그를 나만 옮기는 게 아니니까 다른 사람들도 쓸 수 있겠다 싶어 리드미도 열심히 꾸몄고 형식을 맞춰서 오픈소스로 배포도 했다. 기존 Naver2Tistory의 문제점 이후에 Clean Code, Clean Architecture 같은 개발 서적을 읽고, 객체지향의 5대 원칙을 공부하면서 내가 ..

키보드 디자인 프로그램

생각하게 된 계기 커스텀 스플릿 키보드를 하나 만들려 생각중이다. 그런데 신경써야 하는 것들과 알아야 하는 것들이 너무 많다. 1. PCB 핸드와이어링을 사용하는 경우 스위치와 와이어를 납땜한다. 따라서 스위치와 하우징을 바꾸기 위해서는 납땜을 풀어줘야 하는데.. 이는 미관상 그닥일 뿐만 아니라 스위치 하나 바꾸자고 와이어링을 다시 하는 것은 아닌 것 같다. 따라서, 가능하다면 PCB 기반에 핫스왑 소켓을 사용하는 편이 좋다. 그럴려면 PCB 기판을 설계할 수 있어야 한다. 그러나 기본 지식 없이 PCB 기판 설계를 위해서는 PCB의 기본에 대해 알고 있어야 한다. 회로는 어떻게 짜는지, 풋프린트(외관)은 어떻게 하는지, 하우징과 체결은 어떤 부분에 할 것인지, 칩 위치는 어디에 배치할 것인지, 내가 짠..

[N2T] Naver2Tistory 리팩토링 시작

CS와 OOP, SOLID를 공부하거나 클린 코드 등 여러가지 개발 서적들을 읽으면서 내가 작성한 코드의 부족함을 느꼈다. 특히 Naver2Tistory의 경우 오픈소스로 배포했음에도 필요없는 부분이 많은 것 같아 리팩토링하려 한다. 목표는 [Naver2Tistory 이외에도, 확장성을 고려 + 유지보수하기 쉬운] 코드로 작성하고자 한다. 일단 해야 할 것 같은 부분은 아래 5개정도이다. 주석 삭제. 쓸데없는 주석을 좀 많이 적긴 했다. 공개되는 부분을 제외하고 내부 로직으로 돌아가는 부분은 삭제하는 게 좋을 것 같다. interface, polymorphism, map을 사용하는 방식 등 고민하고 확장성 있게 코드를 작성해 보자. 이 프로그램은 Naver2Tistory이지만 여러 가지 기능이 추가되어 ..

프로젝트 미어캣 후기

https://github.com/osamhack2022/APP_Meerkat_IQDan 후기 거의 1달간 아무것도 안하고 코딩만 한 것 같다. 하면서 재밌었고, 엄청 많이 배우기도 했다. 조금만 생각해 봐도 git git branch 전략, commit message 협업 방식, git push flow(stash-fetch-rebase) commit template react-native hooks, state, component, re-rendering 등 react native의 working 방식 expo typescript node.js node.js의 MVC 구조, env를 이용한 배포 socket.io 채팅 앱의 동작 방식 ORM prisma 보안 종단간 암호화(E2EE), 디피-헬만 알고..

[N2T] Tistory Open API 앱 등록

Naver2Tistory를 사용하기 위해서는 Tistory Open API에 블로그를 등록하고 App ID, Secret Key를 받아오는 과정이 필요하다. 먼저 아래 링크에 접속한다. https://www.tistory.com/guide/api/manage/register TISTORY 나를 표현하는 블로그를 만들어보세요. www.tistory.com 위와 같이 앱을 등록한다. 서비스 URL/CallBack은 Naver2Tistory를 사용할 티스토리 블로그 주소를 입력하면 된다. 등록했다면 앱 관리에 들어가서 설정을 누르자. 위 사진에서 모자이크된 App ID, Secret Key부분을 config.json에 적어넣으면 된다. 나의 경우 이 블로그 ID는 hyelie이고, 위 사진에 있는 App ID..

[N2T] 네이버 에디터와 티스토리 에디터 분석

1. 네이버 에디터 html을 뜯어 보면 아래와 같다. 제일 상위에 se-main-container가 있고, 그 아래에 각각 글, 코드, 이미지 단락들이 존재한다. 좀 더 상세하게 뜯어본 결과, 네이버 블로그 본문의 구조는 아래와 같다. se-main-conatiner ┗ se-component se-text ... (글인 경우) ┗ se-component se-code {코드블럭 종류} (코드인 경우) ┗ se-component se-image ... (이미지인 경우) ┗ se-component se-quotation ... (인용구인 경우) ┗ se-component se-horizontalLine {구분선 종류} (구분선인 경우) ┗ se-component se-table (표인 경우) 네이버 블로..

[N2T] N2T - 네이버 블로그 이사 프로그램

N2T, Naver2Tistory란? 한 줄로 설명하자면 네이버 -> 티스토리 블로그 이사 프로그램입니다. 좀 더 자세하게 설명하자면, 네이버 블로그 링크를 올리면, 해당 포스팅의 내용을 티스토리 에디터에 맞게 형식을 고쳐 업로드 해 주는 프로그램입니다. 필요성 네이버에서 티스토리로 글을 옮길 때, 본문을 Ctrl+C - Ctrl+V를 하게 되면 복사한 글과 티스토리 에디터에 있는 양식에 맞지 않아 글 내용 수정에 애로사항이 생깁니다. 대표적으로 문단 제목 양식, 소스 코드 블럭, 사진과 캡션이 문제가 되고, Table Of Content도 제대로 출력되지 않습니다. 네이버 블로그 글을 티스토리로 복사해 왔을 때 문제점 재현 기능 v1.0.0 네이버 블로그 HTML 및 이미지 저장 티스토리 블로그에 공개..

플젝 아이디어

deep learning / object detection 기반 - 농구 코트 및 사람 인식, 평면도로 바꾸어서 전술 분석 - 미스매치 여부, 전술별로 승률, 득점률 등을 따져서 빅데이터 만들면 재밌지 싶다. - 농구 슛/드리블 폼 분석 - pose 분석으로 가져오기​ 계획 세워주는 프로그램. - 책/일정 입력하면 계획 세워주는 프로그램​ 택시 잡아주는 프로그램. - 현재 위치 기준, 도착지까지 최단시간으로 갈 수 있는 위치로 잡아주는 프로그램. - A에서 B까지 택시타고 갈 때 A에서 택시를 호출하면 택시가 A까지 오는 위치, A에서 택시를 타고 가는 시간이 있다. - 이 시간을 줄이기 위해서 A에서 B 사이에 있는 A'이라는 위치까지 걸어가고, 택시는 A'까지 오게 해서 시간을 최소화 해주는 어플리케..