SAT-Based Bounded Model Checking for RTECTL and Simply-Timed Systems

摘要

We report on a SAT-based bounded model checking (BMC) method for simply-timed systems (i.e., Kripke models where transitions carry a duration, which is an arbitrary natural number) generated by simply-timed automata with discrete data, and properties expressed in the existential fragment of a soft real-time temporal logic (RTECTL). In particular, since in BMC both the system model and the checked property are translated into a Boolean formula to be analysed by a SAT-solver, we introduce a new Boolean encoding of the RTECTL formulae that is particularly optimized for managing quantitative metric temporal operators, typically found in properties of soft real-time systems (simply-timed systems). The proposed BMC algorithm is implemented as a new module of VerICS, and evaluated by means of two scalable scenarios.