길현영 교수의 연구실에서 발표한 논문 "Automatic incremental recomposition algorithm for QoS-aware internet of things service composition"이 "International Journal of Web and Grid Services 2021"에 게재되었다.
웹서비스(Web service)는 웹 기술을 기반으로 하여 machine-to-machine inter-operation을 제공하기 위한 소프트웨어 시스템으로, 서비스 지향 아키텍쳐 (Service-Oriented Architecture)의 서비스(독립적 기능을 가질 수 있는 비즈니스 논리의 기본 단위)를 기본 개념으로 하여 현실화한 기술이다. 현재 웹서비스는 분산시스템이나 Web 환경에서 Service provider가 다수의 client에게 자신의 기능을 사용할 수 있도록 지원하는 Web API 서비스의 형태로 많이 사용되고 있다. 또한 사물인터넷(Internet-of-Things, IoT) 관련한 다수의 연구에서도 각각의 사물의 기능을 하나의 웹 기반 서비스로서 구현하고 상위 구조에서 이러한 서비스 집합을 관리하는 서비스 지향 아키텍쳐 기반 방식을 사용함으로써 좀더 효율성있는 시스템을 구현, 사용한다. 사용자가 원하는 요구사항을 하나의 특정 서비스로 완전히 충족시키지 못하는 경우, 여러 개의 웹서비스들을 합성하게 함으로써 해당 요구사항을 만족시키는 서비스 컴포지션(Service Composition) 기법은 서비스 개발 비용을 낮추고 효율성을 높이는 기법이다. Web 기반의 large scaled computing 환경과 컴퓨팅 리소스가 한정적인 다양한 종류의 IoT 기기 환경에서, 이러한 서비스 컴포지션 문제는 그 활용성이 더욱 높다.
그런데, 다양한 기기들과 자원 한계성을 갖는 IoT 서비스 환경에서는 일시적인 서버 다운, 시스템 과부하, 네트워크 불량 등의 환경적 변화가 발생할 수 있다. 이러한 변화가 발행하였을 때 기존 service composition 문제의 조건이 변하였기 때문에 그 전에 생성한 composite web service는 더 이상 최적의 solution으로 유효하지 못하다. 특히, QoS를 고려하는 service compositon 문제는 사용자가 원하는 목적을 달성하면서도 최적의 QoS값을 갖는 composite service를 구하는 문제로서, 일부의 환경적 조건 변화 때문에 전체 문제를 처음부터 고려하여 최적의 QoS 값을 갖는 솔루션을 찾는 것은 컴퓨팅 시간의 낭비를 초래하게 된다.
본 논문에서는 환경의 변화가 발생하였을 때 QoS를 고려하는 service compositon 문제를 처음부터 다시 풀지 않고 이전 풀이에서의 중간 과정을 최대한 활용하여 최적의 솔루션을 효율적으로 찾아낼 수 있는 incremental re-composition algorithm을 제안하였다. 본 연구에서 제안한 알고리즘은 특히 적은 변화율을 갖는 경우에 기존 알고리즘에 비해 매우 빠르게 최적의 composite service를 찾아냈고, 다수의 경우에서 변화율의 증가에 따라 computing 시간의 선형적 증가세를 보임으로써, 그 효율성을 보였다.
본 연구실은 다양한 네트워크 환경에서 Web- 및 IoT-서비스의 효율적 사용을 위한 자동화된 service discovery & composition에 대한 연구를 AI planning, model checking, Graph theory 기반 기술을 사용하여 진행해왔고, 최근에는 GNN(Graph Neural Network)을 기반으로 Service representation learning 연구와 Stock/Bitcoin price movement prediction에 대한 연구를 진행 중이다.
길현영 교수의 연구실에서 발표한 논문 "Formal Verification of Blockchain Smart Contracts via ATL Model Checking"이 "IEEE Access" 2022년 호에 게재되었다.
논문 사이트로 이동
이더리움과 같은 최신 블록체인 기술은 스마트 컨트랙트 구현에서 Turing-complete한 프로그래밍 언어를 제공함으로써, 특히 신뢰성이 중요한 금융 분야에 적용되게 하였다. 그러나 스마트 컨트랙트의 사소한 에러들은 금전적으로 막대한 손실을 야기하곤 하는데, DAO 오류, Parity multi-signature 오류, integer underflow/ overflow 오류 등이 그 사례이다. DAO 오류의 경우 5000만 달러 상당의 이더를 도난당하게 하여 이더리움이 이더리움과 이더리움 클래식으로 나뉘게 되는 계기를 만들었다. 이러한 스마트 컨트랙트 상의 오류들을 검출하기 위해 정적 프로그램 분석과 정리 증명기법 기반의 연구들이 진행되어왔으나, 정적 프로그램 분석은 사전에 정의된 패턴의 에러만을 검출할 수 있고, 정리 증명기법 기반 연구는 완전 자동화가 불가능하여 전문가의 참여가 필수적이라는 단점을 갖고 있다. 본 연구는 스마트 트랜잭션의 정확성을 검증하기 위해서, ATL (Alternating-time Temporal Logic) 모델체킹 기법을 이용한다. ATL 모델 체킹이란, 검증 대상인 시스템의 모델과 검증하고자 하는 ATL property가 주어지면, 해당 시스템의 모델이 모든 경우에 주어진 ATL property를 만족하는지를 자동적으로 검증하는 기법이다. ATL 모델체커는 주어진 모델이 property를 만족하는 경우에는 true를 리턴하지만 만족하지 않는 경우에는 counter-example을 알려줌으로써, 개발자가 스마트 컨트랙트의 어느 부분에서 오류가 발생하였는지를 알 수 있게 한다.
[그림 1] ATL model checking procedure for solidity contracts
본 연구에서는 주어진 스마트 컨트랙트를 ATL 모델체커로 검증하기 위해서, 이더리움 스마트 컨트랙트에서 주로 사용되는 Solidity 언어를 ATL 모델체커 MCMAS]의 언어로 정확하게 번역할 수 있는 방법론을 제안하고, DAO Attack, TX.ORIGIN Attack, Safe Remote Purchase Contract 등 3가지 사례에 대한 적용을 통해, 본 연구의 방법론이 실제 스마트 컨트랙트 검증에 성공적으로 사용될 수 있음을 보였다. 또한 본 연구실은 블록체인뿐만 아니라 Service composition, Aircraft systems 등 다양한 Software System의 정확성과 안정성에 대한 검증 연구를 해왔고, 최근에는 인공지능 신경망에 대한 검증 연구를 진행 중이다.
김선옥 교수의 연구실에서 발표한 논문 "On the confidence of stereo matching in a deep-learning era: a quantitative evaluation"이 "IEEE Transactions on Pattern Analysis and Machine Intelligence"에 게재되었다.
논문 사이트로 이동
[그림 1] KITTI 2015 및 Middlebury 데이터셋으로 시험한 Qualitative results concerning Census-CBCA 알고리즘
본 논문은 스테레오 매칭을 획득한 깊이 영상의 신뢰도 추정 방법들을 분석한 논문으로 최근 머신러닝 분야의 세계 최고 학술지인 IEEE Transactions on Pattern Analysis and Machine Intelligence (Impact factor: 16.389) 에 게재 승인 받았다. 본 연구는 이탈리아의 볼로냐 대학교(University of Bologna) 연구진과 국내 한국항공대학교, 연세대학교, 고려대학교, 이화여자대학교의 공동 연구로 진행되었으며 기존의 handcrafted feature부터 최근 사용되고 있는 deep learning 기반의 방법 등 약 60여가지 이상의 신뢰도 추정 방법에 대한 실험을 진행하여 결과를 비교 및 분석하였다.
분석 결과, 2019년 세계 최고 컴퓨터비전 학술대회인 IEEE Computer Vision and Pattern Recognition (CVPR)에서 발표된 김선옥 교수의 ‘LAF-Net: Locally Adaptive Fusion Networks for Stereo Confidence Estimation”이 신뢰도 추정에 있어서 가장 뛰어난 성능을 보여줌을 확인하였다.