Modeling and Verifying Uncertainty-Aware Timing Behaviors using Parametric Logical Time Constraint
Fei Gao1,2, Frederic Mallet2, Min Zhang1,3 and Mingsong Chen1,3
1Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China
2Université Cote d’Azur, CNRS, Inria, I3S, Nice, France
3Shanghai Institute of Intelligent Science and Technology, Tongji University, Shanghai, 200062, China
ABSTRACT
The Clock Constraint Specification Language (CCSL) is a logical time based modeling language to formalize timing behaviors of real-time and embedded systems. However, it cannot capture timing behaviors that contain uncertainties, e.g., uncertainty in execution time and period. This limits the application of the language to real-world systems, as uncertainty often exists in practice due to both internal and external factors. To capture uncertainties in timing behaviors, in this paper we extend CCSL by introducing parameters into constraints. We then propose an approach to transform parametric CCSL constraints into SMT formulas for efficient verification. We apply our approach to an industrial case which is proposed as the FMTV (Formal Methods for Timing Verification) Challenge in 2015, which shows that timing behaviors with uncertainties can be effectively modeled and verified using the parametric CCSL.
Keywords: Uncertainty, timing behavior, logical time, parametric CCSL, SMT.
