Towards Scalable Model Checking of Reflective Systems via Labeled Transition Systems

Kenji Tei, Yasuyuki Tahara, Akihiko Ohsuga

Research output: Contribution to journalArticlepeer-review


Reflection is a technique that enables a system to inspect or change its structure and/or behavior at runtime. It is a key enabler of many techniques for developing systems that have to function despite rapidly changing requirements and environments. A crucial issue in developing reflective systems is to ensure the correctness of their behaviors, because object-level behaviors are affected by metalevel behaviors. In this paper, we present an extended labeled transition system (LTS), which we call a metalevel LTS (MLTS), that supports data representation of another LTS for use in modeling a reflective tower. We show that two of the existing state reduction techniques for an LTS (symmetry reduction and divergence-sensitive stutter bisimulation) are also applicable to an MLTS. Then, we introduce two strategies for implementing an MLTS model in Promela, thereby enabling verification with the SPIN model checker. We also present case studies of applying MLTSs to two reflection applications: self-adaptation of a reconnaissance robot system, and dynamic evolution of an Internet-of-things (IoT) system. The case studies demonstrate the applicability of our approach and its scalability improvement through the state reduction techniques.

Original languageEnglish
Pages (from-to)1299-1322
Number of pages24
JournalIEEE Transactions on Software Engineering
Issue number3
Publication statusPublished - 2023 Mar 1


  • Model checking
  • SPIN model checker
  • labeled transition system
  • reflection

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Towards Scalable Model Checking of Reflective Systems via Labeled Transition Systems'. Together they form a unique fingerprint.

Cite this