SMT-based consistency analysis of industrial systems requirements.

As the complexity of industrial systems increases, it becomes difficult to ensure the correctness of system requirements specifications with respect to certain criteria such as consistency. Automated techniques for consistency checking of requirements, mostly by means of model checking, have been proposed in academia. However, such approaches can sometimes be costly in terms of modeling and analysis time or not applicable for certain types of properties. In this paper, we present a complementary method that relies on pattern-based formalization of requirements and automated consistency checking using the state-of-the-art SMT tool Z3. For validation, we apply our method on a set of timed computation tree logic requirements of an industrial automotive subsystem called the Fuel Level Display.