Compositional Reasoning in Model-Based Verification of Adaptive Embedded Systems

摘要

Formal verification of adaptive systems allows rigorously proving critical requirements. However, design-level models are in general too complex to be handled by verification tools directly. To counter this problem, we propose to reduce model complexity on design-model level in order to facilitate model-based verification. First, we transfer existing compositional reasoning techniques for foundational models used in verification tools to design-level models. Second, we develop new compositional strategies exploiting the special features of adaptive models. Based on these results, we establish a framework for modular model-based verification of adaptive systems by model checking.