Runtime Contracts Checker: Increasing Robustness of Component-Based Software Systems

Abstract

Software Systems are becoming increasingly complex leading to new Validation &Verification challenges. Model checking and testing techniques are used at development time while runtime verification aims to verify that a system satisfies a given property at runtime. This second technique complements the first one. This paper presents a runtime contract checker (RCC) which checks a component-based software system's contracts defined at design phase. We address embedded systems whose software components are designed by Unified Modelling Language-State Machines (UML-SM) and their internal information can be observable in terms of model elements at runtime. Our previous research work, CRESCO (C++ REflective State-Machines based observable software COmponents) framework, generates software components that provide this observability. The checker uses software components' internal status information to check system level safety contracts. The checker detects when a system contract is violated and starts a safeStop process to prevent the hazardous scenario. Thus, the robustness of the system is increased.