Formal Model and Method to Decompose Process-Aware IoT Applications | SpringerLink
Skip to main content
Springer Nature Link
Log in

Formal Model and Method to Decompose Process-Aware IoT Applications

  • Conference paper
  • First Online:
On the Move to Meaningful Internet Systems. OTM 2017 Conferences (OTM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10573))

Abstract

The Internet of Things (IoT) integrates a large number of pervasive things that continuously generate data about the physical world. While such generated data can be sent to the Cloud for processing, more and more scenarios are considered where IoT created data will be stored, processed, analyzed, and acted upon close to or at the Edge of the network. Consequently, IoT applications require to be deployed in distributed environments. In this paper, we propose a formal approach for the decomposition of process-aware applications to be deployed in IoT environments. We model process-aware applications in Petri nets, formally define the decomposition process and prove its correctness. As a proof of concept, we have extended the Node-RED tool to allow the modeling, deployment and distributed running of IoT applications.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. van der Aalst, W.M.P., Weske, M.: The P2P approach to interorganizational workflows. In: Bubenko, J., Krogstie, J., Pastor, O., Pernici, B., Rolland, C., Sølvberg, A. (eds.) Seminal Contributions to Information Systems Engineering, 25 Years of CAiSE, pp. 289–305. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. van der Aalst, W., Basten, T.: Inheritance of workflows: an approach to tackling problems related to change. Theoret. Comput. Sci. 270(1), 125–203 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Alferez, M., Tessier, P., Janssens, C., Roubekas, P., Pascual, G., Nicolas Fauvergue, V.L., Damus, C.W., Gurcan, O., Adam, M., Radermacher, A., Tatibouet, J., Geoffroy, J., Maggi, B., Peretokin, V., Dumoulin, C., Letavernier, C., Hafsteinn, Schnekenburger, R., Landre, T., Benois, J.: Papyrus Modeling environment, 1 September 2016. https://eclipse.org/papyrus. Accessed 15 Jan 2017

  4. Amazon: The Amazon Simple Workflow Service developer guide (2016). http://docs.aws.amazon.com/amazonswf/latest/developerguide/swf-welcome.html

  5. Anstett, T., Leymann, F., Mietzner, R., Strauch, S.: Towards BPEL in the cloud: exploiting different delivery models for the execution of business processes. In: 2009 Congress on Services - I, pp. 670–677, July 2009

    Google Scholar 

  6. Barais, O., Tricoire, M., Dartois, J.E., Bourcier, J., Morin, B., Nain, G., Plouzeau, N., Sunye, G., Jezequel, J.M.: The Kevoree Book (2013). http://www.kevoree.org. Accessed 15 Jan 2017

  7. Barcelo, M., Correa, A., Llorca, J., Tulino, A.M., Vicario, J.L., Morell, A.: IoT-cloud service optimization in next generation smart environments. IEEE J. Sel. Areas Commun. 34(12), 4077–4090 (2016)

    Article  Google Scholar 

  8. Best, E., Koutny, M.: Petri net semantics of priority systems. Theor. Comput. Sci. 96(1), 175–215 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  9. Buchholz, P., Kemper, P.: Hierarchical reachability graph generation for petri nets. Form. Methods Syst. Des. 21(3), 281–315 (2002)

    Article  MATH  Google Scholar 

  10. MacGillivray, C., et al.: IDC FutureScape: worldwide Internet of Things 2017 predictions. https://www.idc.com/getdoc.jsp?containerId=US40755816

  11. Ciccozzi, F., Spalazzese, R.: MDE4IoT: supporting the Internet of Things with model-driven engineering. In: Badica, F., et al. (eds.) Intelligent Distributed Computing X. SCI, vol. 678, pp. 67–76. Springer, Cham (2017). doi:10.1007/978-3-319-48829-5_7

    Chapter  Google Scholar 

  12. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)

    Google Scholar 

  13. Cobleigh, J.M., Giannakopoulou, D., PĂsĂreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003). doi:10.1007/3-540-36577-X_24

    Chapter  Google Scholar 

  14. Dornemann, T., Juhnke, E., Freisleben, B.: On-demand resource provisioning for BPEL workflows using Amazon’s elastic compute cloud. In: Proceedings of the 2009 9th IEEE/ACM International Symposium on Cluster Computing and the Grid, CCGRID 2009, pp. 140–147. IEEE Computer Society, Washington, D.C. (2009)

    Google Scholar 

  15. Dumas, M., van der Aalst, W.M., ter Hofstede, A.H.: Process-aware Information Systems: Bridging People and Software Through Process Technology. Wiley Inc., New York (2005)

    Book  Google Scholar 

  16. Fleurey, F., Morin, B.: ThingML: a modeling language for embedded and distributed systems, 20 October 2014. http://thingml.org. Accessed 15 Jan 2017

  17. Foundry, C.: Cloud Foundry official blog. Deploying a service container on CF using the standalone framework (2016). http://blog.cloudfoundry.com/2012/06/18/deploying-tomcat-7-using-the-standalone-framework/

  18. Klai, K., Petrucci, L.: Modular construction of the symbolic observation graph. In: ACSD, pp. 88–97. IEEE (2008)

    Google Scholar 

  19. Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 294–309. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03848-8_20

    Chapter  Google Scholar 

  20. Koutny, M.: Modelling systems with dynamic priorities. In: Rozenberg, G. (ed.) Advances in Petri Nets 1992. LNCS, vol. 609, pp. 251–266. Springer, Heidelberg (1992). doi:10.1007/3-540-55610-9_174

    Chapter  Google Scholar 

  21. Le Cornec, Y.S.: Compositional analysis of modular petri nets using hierarchical state space abstraction. In: Joint 5th International Workshop on Logics, Agents, and Mobility, LAM 2012, the 1st International Workshop on Petri Net-Based Security, WooPS 2012 and the 2nd International Workshop on Petri Nets Compositions, CompoNet 2012, vol. 853 (2012)

    Google Scholar 

  22. McMillan, K.L., Qadeer, S., Saxe, J.B.: Induction in compositional model checking. In: Proceedings of the 12th International Conference on Computer Aided Verification, CAV 2000, Chicago, IL, USA, 15–19 July 2000, pp. 312–327 (2000)

    Google Scholar 

  23. Meyer, S., Ruppen, A., Hilty, L.: The things of the Internet of Things in BPMN. In: Persson, A., Stirna, J. (eds.) CAiSE 2015. LNBIP, vol. 215, pp. 285–297. Springer, Cham (2015). doi:10.1007/978-3-319-19243-7_27

    Chapter  Google Scholar 

  24. Meyer, S., Ruppen, A., Magerkurth, C.: Internet of Things-aware process modeling: integrating IoT devices as business process resources. In: Salinesi, C., Norrie, M.C., Pastor, Ó. (eds.) CAiSE 2013. LNCS, vol. 7908, pp. 84–98. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38709-8_6

    Chapter  Google Scholar 

  25. Miczulski, P.: State space calculation algorithm of hierarchical petri nets with application of decision diagrams. In: DESDes 2001, p. 67 (2001)

    Google Scholar 

  26. Naef, L.: ClickScript, 29 May 2014. https://github.com/lnaef/ClickScript. Accessed 15 Jan 2017

  27. Notomi, M., Murata, T.: Hierarchical reachability graph of bounded petri nets for concurrent-software analysis. IEEE Trans. Softw. Eng. 20(5), 325–336 (1994)

    Article  MATH  Google Scholar 

  28. O’Leary, N., Conway-Jones, D.: Node-RED: a visual tool for wiring the Internet of Things, 11 January 2017. https://nodered.org/. Accessed 15 Jan 2017

  29. Object Management Group: Business process model and notation (BPMN) version 2.0. Technical report formal/2011-01-03. Object Management Group (OMG), January 2011. http://taval.de/publications/BPMN20

  30. Shi, W., Dustdar, S.: The promise of edge computing. Computer 49(5), 78–81 (2016)

    Article  Google Scholar 

  31. Van Der Aalst, W.M.P., Ter Hofstede, A.H.M., Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distrib. Parallel Databases 14(1), 5–51 (2003)

    Article  Google Scholar 

  32. Wagner, S., Kopp, O., Leymann, F.: Towards choreography-based process distribution in the cloud. In: 2011 IEEE International Conference on Cloud Computing and Intelligence Systems, pp. 490–494, September 2011

    Google Scholar 

  33. Xiong, P., Fan, Y., Zhou, M.: A petri net approach to analysis and composition of web services. IEEE Trans. Syst. Man Cybern. Part A 40, 376–387 (2010)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Research - Almaden, 650 Harry Rd, San Jose, CA, 95120, USA

    Samir Tata & Rakesh Jain

  2. LIPN, CNRS UMR 7030, Université Paris 13, Paris, France

    Kais Klai

Authors
  1. Samir Tata
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kais Klai
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Rakesh Jain
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Samir Tata .

Editor information

Editors and Affiliations

  1. University of Lorraine, Nancy, France

    Hervé Panetto

  2. Odisee University College, Brussels, Belgium

    Christophe Debruyne

  3. Télécom SudParis, Évry, France

    Walid Gaaloul

  4. Tilburg University, Tilburg, The Netherlands

    Mike Papazoglou

  5. Freie Universität Berlin and Fraunhofer FOKUS, Berlin, Germany

    Adrian Paschke

  6. Università degli Studi di Milano, Crema, Italy

    Claudio Agostino Ardagna

  7. TU Graz, Graz, Austria

    Robert Meersman

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Tata, S., Klai, K., Jain, R. (2017). Formal Model and Method to Decompose Process-Aware IoT Applications. In: Panetto, H., et al. On the Move to Meaningful Internet Systems. OTM 2017 Conferences. OTM 2017. Lecture Notes in Computer Science(), vol 10573. Springer, Cham. https://doi.org/10.1007/978-3-319-69462-7_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-69462-7_42

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-69461-0

  • Online ISBN: 978-3-319-69462-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation