Abstract
TRIM is a tool for analyzing system requirements expressed using Triggered Message Sequence Charts (TMSCs). TMSCs enhance MSCs with capabilities for expressing conditional and partial behavior and with a refinement ordering. This paper shows how the Concurrency Workbench of the New Century may be adapted to check refinements between TMSC specifications.
Research supported by NSF grants CCR-9988489 and CCR-0098037 and Army Research Office grants DAAD190110003 and DAAD190110019.
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
Center-TRACON automation system (CTAS), http://ctas.arc.nasa.gov/
Integrated Medical Systems Inc., http://www.lstat.com/lstat.html
Message sequence charts (MSC). ITU-TS Recommendation Z.120 (1996)
Abrial, J.R., Börger, E., Langmaack, H.: Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. In: Abrial, J.-R., Börger, E., Langmaack, H. (eds.) Dagstuhl Seminar 1995. LNCS, vol. 1165, Springer, Heidelberg (1996)
Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)
Ben-Abdallah, H., Leue, S.: MESA: Support for scenario-based design of concurrent systems. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 118–135. Springer, Heidelberg (1998)
Cleaveland, R., Madelaine, E., Sims, S.: A front-end generator for verification tools. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 153–173. Springer, Heidelberg (1995)
Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: A semantics based tool for the verification of concurrent systems. ACM TOPLAS 15(1), 36–72 (1993)
Cleaveland, R., Sims, S.: Generic tools for verifying concurrent systems. Science of Computer Programming 42(1), 39–47 (2002)
Plotkin, G.: A structural approach to operational semantics. Technical report, University of Aarhus, Denmark (1981)
Harel, D., Marelly, R.: Specifying and executing behavioral requirements: The play-in/ play-out approach. Software and System Modeling (SoSym) (2003)
Hennessy, M.: Algebraic theory of processes. The MIT Press, Cambridge (1988)
Sengupta, B., Cleaveland, R.: Refinement-based requirements elicitation using triggered message sequence charts. In: To appear in 2003 Intl. Requirements Engineering Conf. (2003)
Sengupta, B., Cleaveland, R.: Triggered message sequence charts. In: Proceedings of ACM SIGSOFT, FSE-10 (2002)
Sengupta, B., Cleaveland, R.: Towards formal but flexible scenarios. In: 2nd International Workshop on Scenarios and State Machines: Models, Algorithms and Tools, ICSE 2003 (2003)
Kramer, J., Uchitel, S., Magee, J.: LTSA-MSC: Tool support for behaviour model elaboration using implied scenarios. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vos. 2619, pp. 597–601. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sengupta, B., Cleaveland, R. (2003). TRIM: A Tool for Triggered Message Sequence Charts. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive