Abstract
We propose an approach to automatic verification of real-time systems against scenario-based requirements. A real-time system is modeled as a network of Timed Automata (TA), and a scenario-based requirement is specified as a Live Sequence Chart (LSC). We define a trace-based semantics for a kernel subset of the LSC language. By equivalently translating an LSC chart into an observer TA and then non-intrusively composing this observer with the original system model, the problem of verifying a real-time system against a scenario-based requirement reduces to a classical real-time model checking problem. We show how this is accomplished in the context of the Uppaal model checker.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)
Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Bontemps, Y.: Relating Inter-Agent and Intra-Agent Specifications: The Case of Live Sequence Charts. PhD thesis, University of Namur (2005)
Bontemps, Y., Schobbens, P.-Y.: The computational complexity of scenario-based agent verification and design. J. Applied Logic 5(2), 252–276 (2007)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19(1), 45–80 (2001)
Damm, W., Toben, T., Westphal, B.: On the Expressive Power of Live Sequence Charts. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Wilhelm Festschrift. LNCS, vol. 4444, pp. 225–246. Springer, Heidelberg (2007)
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)
Genest, B., Minea, M., Muscholl, A., Peled, D.: Specifying and Verifying Partial Order Properties Using Template MSCs. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 195–210. Springer, Heidelberg (2004)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Foundations of Computer Science 13(1), 5–51 (2002)
ITU: Z. 120 ITU-TS Recommendation Z.120: Message Sequence Chart 2000 (1999)
Klose, J., Wittke, H.: An Automata Based Interpretation of Live Sequence Charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 512–527. Springer, Heidelberg (2001)
Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y.: Temporal Logic for Scenario-Based Specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005)
Lahtinen, J.: Model checking timed safety instrumented systems. Research Report TKK-ICS-R3, Helsinki University of Technology, Espoo, Finland (2008)
Pusinskas, S.: From Live Sequence Charts to Uppaal. PhD thesis (forthcoming)
Rye-Andersen, J.G., Jensen, M.W., Goettler, R., Jakobsen, M.: PEEL: Property Extraction Engine for LSCs. Master thesis, Aalborg University (2004)
Sengupta, B., Cleaveland, R.: Triggered Message Sequence Charts. In: FSE (2002)
Yovine, S.: Kronos: A verification tool for real-time systems. STTT 1(1/2), 123–133 (1997)
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
Larsen, K.G., Li, S., Nielsen, B., Pusinskas, S. (2009). Verifying Real-Time Systems against Scenario-Based Requirements. In: Cavalcanti, A., Dams, D.R. (eds) FM 2009: Formal Methods. FM 2009. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05089-3_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-05089-3_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05088-6
Online ISBN: 978-3-642-05089-3
eBook Packages: Computer ScienceComputer Science (R0)