Context-Aware Verification of a Cruise-Control System

摘要

Despite the high-level of automation, the practicability of model-checking large asynchronous models is hindered by the state-space explosion problem. To address this challenge the Context-aware Verification technique relies on the identification and explicit specification of the environment (context) in which the system-under-study operates. In this paper we apply this technique for the verification of a Cruise-control System (CCS). The asynchrony of this system renders traditional model-checking approaches almost impossible. Using the Context-aware Verification technique this task becomes manageable by relying on two powerful optimisation strategies enabled by the structural properties of the contexts: automatic context-splitting, a recursive state-space decomposition strategy; context-directed semi-external reachability analysis, an exhaustive analysis technique that reduces the memory pressure during verification through the use of external memory. In the case of the CCS system, this approach enabled the analysis of up to 5 times larger state-spaces than traditional approaches.