Advertisement

TASS: Timing Analyzer of Scenario-Based Specifications

  • Minxue Pan
  • Lei Bu
  • Xuandong Li
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

In this paper, we present TASS which is a timing analyzer of scenario-based specifications. TASS accepts UML2.0 interaction models with general and expressive timing constraints and can be used for three kinds of timing analysis problems: the reachability analysis, the constraint conformance analysis, and the bounded delay analysis. The underlying technique of TASS is to reduce the timing analysis problems into linear programming problems.

Keywords

Model Check Sequence Diagram Reachability Analysis Java Virtual Machine Bound Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    ITU-TS. ITU-T. Recommendation Z.120. ITU - Telecommunication Standardization Sector, Geneva, Switzerland (May 1996)Google Scholar
  2. 2.
    Object Management Group, Framingham, Massachusetts. UML 2.0 Superstructure Specification (October 2004)Google Scholar
  3. 3.
    Alur, R., Holzmann, G., Peled, D.: An analyzer for message sequence charts. Tools and Algorithms for the Construction and Analysis of Systems, 35–48 (1996)Google Scholar
  4. 4.
    Ben-Abdallah, H., Leue, S.: Timing Constraints in Message Sequence Chart Specifications. In: Proc. of FORTE X/PSTV XVII, pp. 91–106. Chapman & Hall, Boca Raton (1998)Google Scholar
  5. 5.
    Seemann, J., von Gudenberg, J.W.: Extension of UML Sequence Diagrams for Real-Time Systems. In: Bézivin, J., Muller, P.-A. (eds.) UML 1998. LNCS, vol. 1618, pp. 240–252. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  6. 6.
    Firley, T., Huhn, M., Diethers, K., Gehrke, T., Goltz, U.: Timed sequence diagrams and tool-based analysis - A case study. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 645–660. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Li, X., Lilius, J.: Timing analysis of UML sequence diagrams. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 661–674. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Li, X., Lilius, J.: Checking compositions of UML sequence diagrams for timing inconsistency. In: Proc. of APSEC 2000, pp. 154–161. IEEE Computer Society, Los Alamitos (2000)Google Scholar
  9. 9.
    Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Form. Methods Syst. Des. 1, 385–415 (1992)CrossRefzbMATHGoogle Scholar
  10. 10.
    Alur, R., Yannakakis, M.: Model Checking of Message Sequence Charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, p. 114. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  11. 11.
    Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)Google Scholar
  12. 12.
    Li, X., Pan, M., Bu, L., Wang, L., Zhao, J.: Timing Analysis of Scenario-Based Specifications (manuscript), http://cs.nju.edu.cn/lxd/TASS/
  13. 13.
  14. 14.
    Ladkin, P., Leue, S.: Interpreting Message Sequence Charts. Technical Report TR 101, Dept. of Computing Science, University of Stirling, United Kingdom (1993)Google Scholar
  15. 15.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126 (1994)Google Scholar
  16. 16.

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Minxue Pan
    • 1
    • 2
  • Lei Bu
    • 1
    • 2
  • Xuandong Li
    • 1
    • 2
  1. 1.State Key Laboratory for Novel Software TechnologyNanjing UniversityChina
  2. 2.Department of Computer Science and TechnologyNanjing UniversityNanjingP.R. China

Personalised recommendations