A framework for the specification and validation of dynamic reconfigurable systems

We study a framework for the specification and validation of dynamic reconfigurable systems. The framework is based on configuration logic for the description of architecture styles which are families of architectures sharing common connectivity features. We express specifications in the Temporal Configuration Logic (TCL), a linear time temporal logic built from atomic formulas characterizing system configurations and temporal modalities. Two non-trivial benchmarks are introduced to show the adequacy of TCL for the specification of dynamic reconfigurable systems. We study an effective model-checking procedure based on SMT techniques for a non-trivial fragment of TCL which has been implemented in a prototype runtime verification tool. We provide preliminary experimental results illustrating the capabilities of the tool on the considered benchmark systems.

Discrete Fault Diagnosis of Structurally Reconfigurable Systems

Fault diagnosis of a certain class of hybrid systems referred to as Structurally Reconfigurable (SR) systems is complicated. This is because SR systems tend to switch their configuration which may or may not be faulty. It is important to identify the mode of the SR system along with the corresponding fault if any, in order to facilitate a fault tolerant action. This paper combines discrete fault diagnosis with mode identification for SR systems to achieve two main objectives: Sensor selection for fault detection, isolation and mode identification, and residual selection for mode identification. The framework is built using a structural analysis based approach to meet these objectives. This framework is demonstrated for a 10-Speed Automatic Transmission, which is an illustrative example of SR systems.