Skip to main content
SpringerLink
Log in

MDE-Based Verification of SysML State Machine Diagram by UPPAAL

  • Conference paper
Trustworthy Computing and Services (ISCTCS 2012)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 320))

Included in the following conference series:

Abstract

State Machine Diagram (SMD) is one of the SysML behavior diagrams, but it is a kind of semi-formal model language. As a consequence, models can not be verified conveniently and efficiently, especially in real-time embedded system (RTES) field as there are no descriptions of time and probability in SMD. To address these problems, we extend SMD with time and probability elements extracted from MARTE and propose a transformation algorithm based on MDE. With the algorithm, we transform the extended SMD to timed automata (TA) and then analyze and verify the transformation result using existing tools. So at the very beginning of system design, errors and deficiencies can be found. At last, we construct an instance to illustrate the validity of our approach.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. OMG: Systems Modeling Language. Formal/2010-06-01 (2010), http://www.omg.org/spec/SysML/1.2

  2. OMG: UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded systems. Formal/2011-06-02 (2011), http://www.omg.org/spec/MARTE/1.1

  3. ATLAS Team. ATLAS Transformation Language (ATL) Home Page, http://www.eclipse.org/gmt/atl/

  4. Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–236 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. OMG/RFP/QVT MOF 2.0 query/views/transformations RFP. Formal/2011-01-01 (2011), http://www.omg.org/spec/QVT/1.1

  6. OMG: Object Constraint Language. Formal/2006-05-01 (2006), http://www.omg.org/spec/OCL/2.0

  7. Zhang, T., Jouault, F., Attiogb, C., Li, X.D.: MDE-based mode transformation: from MARTE model to FIACRE model. Journal of Software 20(2), 214–233 (2009)

    Article  Google Scholar 

  8. Gu, Z.H., Shin, K.G.: An Integrated Approach to Modeling and Analysis of Embedded Real-Time Systems Based on Timed Petri Nets. In: Proceedings of Distributed Computing Systems, pp. 350–359 (2003)

    Google Scholar 

  9. Cortés, L.A., Eles, P., Peng, Z.B.: Verification of embedded systems using a petri net based representation. In: Proceedings of the 13th International Symposium on System Synthesis, ISSS (2000)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  12. Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. In: Proceedings of the 18th IEEE Real-Time Systems Symposium, pp. 2–13 (1997)

    Google Scholar 

  13. ATLAS group LINA and INRIA.: ATL: Atlas Transformation Language (2006)

    Google Scholar 

  14. Budinsky, F., Steinberg, D., Merks, E., Ellersick, R., Timothy, J.: Eclipse Modeling Framework: A Developer’s Guide, p. 704. Addison-Wesley Professional (2003)

    Google Scholar 

  15. Tan, H.B., Yao, S.Z., Li, W.Y.: Modeling Time-Triggered Mechanisms using MARTE. In: Information Science and Engineering (ICISE), pp. 4590–4593 (2010)

    Google Scholar 

  16. Katz, S., Grumberg, O.: A Framework for Translating Models and Specifications. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 145–164. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Cui, K.L., Yang, Z.Y., Xie, J.K., Wan, K.Y.: Unifying Modeling and Simulation Based on UML Timing Diagram and UPPAAL. In: Proceedings of ICCMS (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Lab. for Novel Software Technology, Nanjing University, Nanjing, China

    Xiaopu Huang, Qingqing Sun, Jiangwei Li & Tian Zhang

  2. Department of Computer Science and Technology, Nanjing University, Nanjing, China

    Xiaopu Huang, Qingqing Sun, Jiangwei Li & Tian Zhang

Authors
  1. Xiaopu Huang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Qingqing Sun
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jiangwei Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tian Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Beijing University of Posts and Telecommunications, Beijing, China

    Yuyu Yuan  & Xu Wu  & 

  2. The School of Telecommunications Engineering, Beijing University of Posts and Telecommunications Beijing, P. O. Box 128, 100876, Beijing, China

    Yueming Lu

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Huang, X., Sun, Q., Li, J., Zhang, T. (2013). MDE-Based Verification of SysML State Machine Diagram by UPPAAL. In: Yuan, Y., Wu, X., Lu, Y. (eds) Trustworthy Computing and Services. ISCTCS 2012. Communications in Computer and Information Science, vol 320. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35795-4_62

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-35795-4_62

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-35794-7

  • Online ISBN: 978-3-642-35795-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation