Verification and abstraction of real-time variability-intensive systems

Featured timed automaton (FTA) is a concise formalism to model the real-time behaviour of variability-intensive systems. FTA extends the timed automaton by allowing optional transitions and clock constraints that are relevant only for a subset of the system variants. Then, one can verify a variant individually by deriving the corresponding TA from the FTA and using established tools like UPPAAL or apply family-based algorithms to verify all variants at once. These latter algorithms consist of computing the reachability relation in FTA as an antichain. Yet, they suffer from a three-source complexity: the number of states, the number of time clocks and the number of variants. This motivates the design of abstraction refinement heuristics to reduce verification effort. In this paper, we present the syntax and semantics of FTA, efficient algorithms to compute their reachability relations, and discuss how abstraction methods can be applied.