Towards Scalable Model Checking of Reflective Systems via Labeled Transition Systems

Kenji Tei, Yasuyuki Tahara, Akihiko Ohsuga

研究成果: Article査読

1 被引用数 (Scopus)

抄録

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.

本文言語English
ページ(範囲)1299-1322
ページ数24
ジャーナルIEEE Transactions on Software Engineering
49
3
DOI
出版ステータスPublished - 2023 3月 1

ASJC Scopus subject areas

  • ソフトウェア

フィンガープリント

「Towards Scalable Model Checking of Reflective Systems via Labeled Transition Systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル