Overview  

TASS is a Timing Analyzer of Scenario-based Specifications. Scenario-based specifications (SBSs) such as MSC specifications and UML interaction models offer an intuitive and visual way of describing design requirements. Such specifications can describe concrete interactions among communicating entities and therefore are playing an increasingly important role in the design of software systems. Like any other aspect of the specification and design process, SBSs are amenable to errors, and their analysis is important. We present TASS for the verification and analysis of the timing properties of SBSs.

TASS supports two mainstream SBSs: The UML interaction models and the MSC specifications. The UML interaction models consist of UML sequence diagrams and a UML2.0 interaction overview diagram. The MSC specifications consist of basic MSCs and a High-level MSC. Both SBSs support hierarchical modelling.

TASS supports both synchronous and asynchronous compositional semantics. Under synchronous concatenation, TASS provides a decision procedure for Loop-unlimited SBSs; while under asynchronous concatenation, TASS provides a decision procedure for Flexible Loop-closed SBSs.

TASS provides solutions to various timing analysis problems. TASS can be used to solve the reachability analysis, the constraint conformance analysis and the bounded delay analysis problems for SBSs with synchronous concatenation; and the reachability analysis and the bounded delay analysis problems for SBSs with asynchronous concatenation.

TASS supports bounded model checking. For general SBSs, TASS provides a path-oriented timing analyzer to check one single finite path, a bounded timing analyzer to check the whole SBSs in a given threshold, which can increase the faith in the correctness of the system.

Detailed technical background can be found in our recent publications.

Publications

• Minxue Pan, Xuandong Li. Timing Analysis of MSC Specifications with Asynchronous Concatenation.
• Xuandong Li, Minxue Pan, Lei Bu, Linzhang Wang, Jianhua Zhao. Timing Analysis of Scenario-Based Specifications using Linear Programming. In Software Testing, Verification and Reliability, Wiley InterScience, 2010, Published online: DOI: 10.1002/stvr.434.
• Minxue Pan, Lei Bu, Xuandong Li. TASS: Timing Analyzer of Scenario-Based Specifications. In Proceedings of the 21th International Conference on Computer Aided Verification (CAV2009), France, 2009, Lecture Notes in Computer Science 5643, Springer, pp.689-695.

Download

TASS is available now! You may download TASS via the download page. We have implemented two versions. One is an Eclipse plugin which is an integrated environment for modelling and analysis. The other is a Java standalone application which reads models generated by Rational Rose. We also provide details of two well-known examples which are the automatic teller machine (ATM) system and the global system for mobile communication (GSM). They can be found in the case study pages.