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.
Chapter PDF
Similar content being viewed by others
Keywords
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
ITU-TS. ITU-T. Recommendation Z.120. ITU - Telecommunication Standardization Sector, Geneva, Switzerland (May 1996)
Object Management Group, Framingham, Massachusetts. UML 2.0 Superstructure Specification (October 2004)
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)
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)
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)
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)
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)
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)
Courcoubetis, C., Yannakakis, M.: Minimum and maximum delay problems in real-time systems. Form. Methods Syst. Des. 1, 385–415 (1992)
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)
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 118–149 (2003)
Li, X., Pan, M., Bu, L., Wang, L., Zhao, J.: Timing Analysis of Scenario-Based Specifications (manuscript), http://cs.nju.edu.cn/lxd/TASS/
OR-Objects, http://OpsResearch.com/OR-Objects/index.html
Ladkin, P., Leue, S.: Interpreting Message Sequence Charts. Technical Report TR 101, Dept. of Computing Science, University of Stirling, United Kingdom (1993)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126 (1994)
TASS Website, http://cs.nju.edu.cn/lxd/TASS/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pan, M., Bu, L., Li, X. (2009). TASS: Timing Analyzer of Scenario-Based Specifications. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_56
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_56
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)