디지털 라이브러리[ 검색결과 ]
ILP 기반한 시간민감네트워크 스케줄 생성
http://doi.org/10.5626/JOK.2021.48.6.595
최신 실시간 이더넷 표준인 IEEE 802.1Qbv 시간민감네트워크(Time Sensitive Network, 이하 TSN)는 스트림의 시간적 정확성을 보장하기 위해 고안된 네트워크의 표준이다. TSN은 공장 자동화나 자동차 네트워크 시스템을 대체할 이더넷 기반 네트워크로 현재 개발되고 있다. TSN은 오프라인 상에서 만들어진 스케줄에 근거하여 스트림의 흐름을 제어함으로써 주어진 스트림의 종단간지연 혹은 지터 요구사항을 만족시킬 수 있다. 하지만 TSN 스케줄 생성은 NP-hard 문제로 그 복잡도에 있어서 매우 풀기 어려운 문제이다. 그러한 이유로 최근에는 SMT(Satisfiability Modulo Theory)이나 ILP(Integer Linear Programming) 같은 제약사항 해결 기법(Constraint solving technique) 등이 해결방법으로 제시되고 있다. 이 논문에서는 오프라인 상에서의 생성하는 TSN 스케줄 생성을 위해 휴리스틱과 ILP를 함께 이용한 탐욕적이며 점증적인(greedy and incremental) 알고리즘을 제공한다. 이렇게 하여 계산 복잡도를 줄이고 스케줄 생성 성능을 높이고자 한다. 본 논문에서는 특히 기존의 SMT 솔버를 통한 접근과의 비교를 통해 본 연구에서 제시하는 방법에 대한 성능을 비교한다.
Coq에서의 실시간 분산 시스템 검증을 위한 네트워크 및 운영체제 행동의 정형 모델 정의
http://doi.org/10.5626/JOK.2020.47.11.1071
정형 검증을 적용하여 분산 시스템의 안전성을 높이는 것은 중요한 과제이다. 분산 시스템 중 항공, 의료기기와 같은 안전 우선 시스템은 안전성의 위협이 큰 사고와 직결될 수 있다. 하지만 분산 시스템을 정형 검증하기 위해서는 소프트웨어의 실행 의미뿐만 아니라, 소프트웨어를 실행시키는 운영체제와 메시지를 전달하는 네트워크의 환경 등에 대한 기술이 필요하다. 우리는 Coq 증명 보조 도구 안에서 네트워크와 운영체제의 추상적인 행동에 대한 모델을 정의하였다. 이 모델은 단계적으로 네트워크 각 지역의 실행 규칙을 제시하고, 이로부터 전체 시스템의 행동을 구성한다. 우리는 이 모델이 실제로 분산 시스템 검증에 유용하게 사용될 수 있음을 보이기 위해 간단한 서버-클라이언트 시스템 검증을 수행하였으며, 이후 실용적인 소프트웨어 검증에 적용되기를 기대하고 있다.
