A Formal Passive Testing Approach for Checking Real Time Constraints

Increasing complexity and distribution of current software systems lead to new and more complex behavioral constraints. Consequently, testing if a given system fulfills its functional requirements becomes more crucial than ever and necessitates more powerful test oracles. In this paper, we focus on temporal requirements of critical systems. We propose a formal testing approach for specification and verification of real time properties. We specify system requirements as XCTL (eXplicit Clock Temporal Logic) formulas and propose a passive testing algorithm to check their conformance w.r.t. collected traces. Our main objective in this work, is to be able to address complex temporal properties. Particularly, we show that our approach can be used to check time correlated constraints which are temporal constraints defined w.r.t. other temporal constraints in the same formula. We also present a case study on Web services to illustrate our approach and discuss the obtained experimental results.