Towards scalable model checking of reflective systems via labeled transition systems

Kenji Tei, Yasuyuki Tahara, Akihiko Ohsuga

Research output: Contribution to journalArticlepeer-review

Abstract

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)1
Number of pages1
JournalIEEE Transactions on Software Engineering
DOIs
Publication statusAccepted/In press - 2022

Keywords

  • Adaptation models
  • Computer architecture
  • labeled transition system
  • model checking
  • Model checking
  • Poles and towers
  • Reconnaissance
  • reflection
  • Robots
  • SPIN model checker
  • Task analysis

ASJC Scopus subject areas

  • Software

Fingerprint

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