Improving timing analysis effectiveness for scenario-based specifications by combining SAT and LP techniques

Open environmental software systems are often time-sensitive, as they need to respond to other entities within the systems and/or in the environments promptly. The timing requirements are therefore an essential part of the system correctness. Scenario-based specifications (SBS) such as message sequence charts and UML interaction models play an important role in specifying open environmental software systems since they intuitively model interactions between different entities. While modelling these systems, the timing requirements can be specified as timing constraints. In this paper, we study the problem of checking the timing consistency of SBS with timing constraints. Although this problem can be transformed into a reachability analysis problem, checking its reachability can still be time-consuming. Therefore, we propose a novel SAT and linear programming (LP) collaborative timing analysis approach named Tassat for the bounded timing analysis of SBS. Instead of using depth-first traversal algorithms, Tassat encodes the structures of the SBS into propositional formulas and adopts SAT solvers to find candidate paths. The timing analysis of candidate paths is then transformed to LP problems, where the irreducible infeasible set of the infeasible paths can be utilized to filter out candidate paths for checking. In addition, we propose an enhanced version of the approach that extends the bounded analysis results to the entire models if the infeasible path segments do not contain intermediate loops. The enhanced algorithm can prove that the given SBS satisfy the required properties on any bound condition. The experimental results show that Tassat is effective and has better performance than existing tools in terms of both time consumption and memory footprint.