Skip to main content

Formal Methods and Embedded System Verification

We translate requirements and designs into mathematical models to analyse them, and verify the actual code in usage logs and simulation environments. This is the lab's oldest line, running since 1994.

Background​

Defects in embedded software are harder to catch when they come from interaction between components than when a single function is written wrong. Indirect dependencies, where several modules share a global variable or one sensor's reading changes the conditions under which another operates, do not show up by reading the code. And they only reproduce under a specific execution order.

The other constraint is the target hardware. Software for appliances, vehicles, or naval combat systems needs the physical equipment to run, each test costs a lot, and early in development the equipment does not exist at all. Deferring verification means design defects surface only at integration.

Approach​

Formal Analysis with Petri Nets​

Requirements and distributed processes are moved into modular Petri nets so reachability and safety can be analysed. Safety is checked not only by forward reachability but also by backward analysis that traces upward from a hazardous state. To handle state explosion we studied slicing, which cuts a model so only part of it is analysed, together with parallel traversal of the state space of concurrent finite state machines. This extended into integrating use cases as modular Petri nets so interactions can be analysed at the requirements stage.

LTS-Based Compositional Safety and Timing Analysis​

A distributed embedded system cannot be verified by merging every component into one model: the state count becomes unmanageable. We worked on compositional verification, which reduces components under LTS equivalence before composing upward, and on synthesising and checking real-time timing constraints with modular TER nets.

Interaction-Based Integration Testing​

Test cases already written for unit testing are characterised by execution path and reused at integration to build function interaction test sequences. The goal is to find indirect interactions that never appear as a direct call, by following definition-use patterns of global variables and data flow. Fault injection then confirms whether such a path actually causes a failure.

Usage Log-Based Testing​

Logs left behind during real operation are turned back into per-input behaviour models, and combinatorial analysis finds dependencies between environmental components that have not yet been exercised, adding tests for them. The target is failures caused by wrong assumptions about the environment, where the code is correct but the surroundings differ. We also built a framework that turns the same logs back into unit test harnesses.

SiL Simulation-Based Verification​

Software is run on a PC and verified without physical equipment. For AUTOSAR components we modified the OSEK operating system so that unit tests run on a virtual prototype, and we applied SiL testing tools to refrigerator and washing machine control software to cut testing time. We also worked on a RIOS-based approach that folds testing and monitoring into the application structure itself.

Selected Records​

The list below is a selection. Some records sit on the boundary between areas, so it is not exhaustive; the full list is in the Archive. Titles and author names are kept in their original language.

  • 환경의 특성을 고려하는 입력 로그 기반의 임베디드 소프트웨어 테스팅PhD Thesis

    정수용

    경북대학교, 2022

    Full text ↗

  • Usage Log-Based Testing of Embedded Software and Identification of Dependencies among Environmental ComponentsInternational JournalIF 0.695

    Sooyong JEONG, Sungdeok CHA, Woo Jin LEE

    IEICE Transactions on Information and Systems, Vol. E104.D, No. 11, pp. 2011-2014, 2021-11-1

    DOI ↗

  • A Log-Based Testing Approach for Detecting Faults Caused by Incorrect Assumptions About the EnvironmentInternational JournalIF 0.449

    Sooyong JEONG, Ajay Kumar JHA, Youngsul SHIN, Woo Jin LEE

    IEICE Transactions on Information and Systems, Vol. E103.D, No. 1, pp. 170-173, 2020-1-1

    DOI ↗

  • Integration testing based on indirect interaction for embedded systemInternational Journal

    Muhammad Iqbal Hossain, Woo Jin Lee

    International Journal of Reconfigurable and Embedded Systems (IJRES), Vol. 8, No. 2, pp. 86, 2019-7-1

    DOI ↗

  • RIOS 기반 임베디드 시스템 소프트웨어 테스트 장치 및 방법Patent GrantedDomestic

    이성희, 이우진

    Granted 10-2025553 (2019-09-26)

    Full text ↗

  • 임베디드 시스템의 통합 테스팅에서의 데이터 흐름 기반 간접 상호작용 테스팅PhD Thesis

    Muhammad Iqbal Hossain

    경북대학교, 2018

    Full text ↗

  • 냉장고 제어 소프트웨어 테스팅 시간 단축을 위한 SIL 테스팅 도구 개발MS Thesis

    서보영

    경북대학교, 2017

    Full text ↗

  • 임베디드 시스템의 결함주입 기반 간접 상호작용 테스팅 기법Domestic Journal

    Muhammad Iqbal Hossain, 이우진

    정보처리학회논문지. 소프트웨어 및 데이터공학, Vol. 6, No. 9, pp. 419-428, 2017-09

    DOI ↗

  • An automated testing method for AUTOSAR software components based on SiL simulationInternational Conference

    Sooyong Jeong, Woo Jin Lee

    2017 Ninth International Conference on Ubiquitous and Future Networks (ICUFN), Milan, Italy, pp. 278-283, 2017-07

    DOI ↗

  • 세탁기 임베디드 소프트웨어 단위 및 통합 테스트 가상환경 구축MS Thesis

    장영근

    경북대학교, 2016

    Full text ↗

  • 임베디드 소프트웨어 단위 테스트를 위한 로그 기반 테스팅 장치 및 그 방법Patent GrantedDomestic

    류호동, 이우진

    Granted 10-1648307 (2016-08-23)

    Full text ↗

  • A Testing Method for AUTOSAR Software Components Using Virtual Prototyping by Modification of OSEK Operating SystemInternational Journal

    Hodong Ryu, Sooyong Jeong, Woo Jin Lee

    pp. 899-905, 2015

    DOI ↗

  • 임베디드 소프트웨어의 단위 테스팅을 위한 로그 기반의 테스팅 프레임워크 개발PhD Thesis

    류호동

    경북대학교, 2015

    Full text ↗

  • 단위 테스트 케이스 재사용 기반의 함수 테스트 장치 및 그 함수 테스트 방법Patent GrantedDomestic

    이우진, 신영술

    Granted 10-1410099-0000 (2014-06-25)

    Full text ↗

  • Integration testing through reusing representative unit test cases for high-confidence medical softwareInternational Journal

    Youngsul Shin, Yunja Choi, Woo Jin Lee

    Computers in Biology and Medicine, Vol. 43, No. 5, pp. 434-443, 2013-6

    DOI ↗

  • A Function Interaction Testing by Reusing Characterized Test CasesInternational Journal

    Youngsul SHIN, Woo Jin LEE

    IEICE Transactions on Information and Systems, Vol. E95.D, No. 9, pp. 2232-2234, 2012

    DOI ↗

  • Test Case Generation Considering Definition-Use of Global Variables for Integration TestingInternational Conference

    Muhammad Iqbal Hossain, Woo Jin Lee

    Jeju Island, Korea, 2012-07-16

    Full text ↗

  • Modeling and Analysis of System Behaviors Using Dynamic Petri netsMS Thesis

    Thi Ly Cao

    경북대학교, 2011

    Full text ↗

  • 병행적 유한상태머신의 상태폭발 완화를 위한 병렬적 상태 공간 순회 기법MS Thesis

    이정선

    경북대학교, 2010

    Full text ↗

  • Safety Property Analysis Techniques for Cooperating Embedded Systems Using LTSInternational Journal

    Woo Jin Lee, Ho-Jun Kim, Heung Seok Chae

    pp. 114-124, 2007

    DOI ↗

  • Synthesis and Analysis of Timing Constraints for Real-Time Embedded Systems using Modular TER netsInternational Journal

    Woo Jin Lee, Ho Kyoung Lee

    WSEAS Transactions on Computers, Vol. 6, No. 5, pp. 741-748, 2007-05

    Full text ↗

  • 내장형 소프트웨어 시스템의 역방향 안전성 분석 방법 및 그 장치Patent GrantedDomestic

    이우진, 임채덕, 김흥남

    Granted 1003162460000 (2001-12-12)

    Full text ↗

  • A Slicing-based approach to enhance Petri Net Reachability AnalysisInternational Journal

    W.J. Lee, S.D. Cha, H.N. Kim, Y.R. Kwon

    Australian Computer Journal, Vol. 32, No. 2, pp. 131-143, 2000-05

  • Analysis of functional requirements using constraints-based modular Petri NetsPhD Thesis

    Woo Jin Lee

    한국과학기술원(KAIST), 전산학과, 1999

    Full text ↗

  • CPN 모델의 역방향 안전성 분석 도구 개발Domestic Journal

    이우진, 채흥석, 차성덕, 이장수, 권용래

    한국정보과학회논문지:컴퓨팅의 실제 및 레터, Vol. 5, No. 4, pp. 457-466, 1999-08

    Full text ↗

  • Integration and analysis of use cases using modular Petri nets in requirements engineeringInternational Journal

    Woo Jin Lee, Sung Deok Cha, Yong Rae Kwon

    IEEE Transactions on Software Engineering, Vol. 24, No. 12, pp. 1115-1130, 1998

    DOI ↗

  • 분산 임베디드 소프트웨어의 실행로그 기반 테스팅 프레임워크Research Project

    2017-06-01 ~ 2022-02-28, 한국연구재단, 연구책임자, KRW 37500K

  • 스마트 자동차를 위한 AUTOSAR 기반 차량 내외부 통신 플랫폼 및 응용 기술Research Project

    2011-05 ~ 2016-12

  • 역공학 기반 임베디드 소프트웨어의 신뢰성 향상 및 테스팅 자동화 연구Research Project

    2010-05-01 ~ 2013-04-30, 한국연구재단, 연구책임자, KRW 55001K

  • 소나체계 데이터 전송 시스템 설계 검증 기법 연구Research Project

    2009-09-01 ~ 2012-12-30, 국방과학연구소(ADD-진해), 연구원

  • 차량 전장용 실시간 운영체제의 국제표준 적합성 인증 연구Research Project

    2009-05-01 ~ 2009-11-30, ETRI, 연구책임자, KRW 20000K

  • S/W modeling & verification with formal methodResearch Project

    2007-04-20 ~ 2007-10-20, LG전자, 연구책임자, KRW 15000K

  • 고신뢰도 내장형 실시간 소프트웨어 개발 기술Research Project

    2006-09 ~ 2011-12, 국방과학연구소

  • 분산 임베디드 시스템의 모델링 및 안전성 분석방법에 관한 연구Research Project

    2005-01-19 ~ 2006-01-18, 한국학술진흥재단, 연구책임자