Skip to main content
SpringerLink
Log in

Introduction

  • Chapter
  • First Online:
Integrated Model of Distributed Systems

Part of the book series: Studies in Computational Intelligence ((SCI,volume 817))

  • 320 Accesses

Abstract

The author’s experience with building industrial and research distributed systems showed that proper modeling and verification of such systems is crucial for their quality.

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 EPUB and 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
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    Yet, in general it is not necessary for a process to return to the calling server.

  2. 2.

    We call the formulas “general”, because “universal formulas” usually refer to those containing the universal quantifier.

  3. 3.

    Note that we do not use the term “state” to avoid ambiguity.

References

  • Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183–235. https://doi.org/10.1016/0304-3975(94)90010-8.

    Article  MathSciNet  MATH  Google Scholar 

  • Balan, M. S. (2009). Serializing the parallelism in parallel communicating pushdown automata systems. Electronic Proceedings in Theoretical Computer Science, 3, 59–68. https://doi.org/10.4204/EPTCS.3.5.

    Article  Google Scholar 

  • Baier, C., & Katoen, J.-P. (2008). Principles of model checking. Cambridge, MA: MIT Press. ISBN: 9780262026499.

    MATH  Google Scholar 

  • Behrmann, G., David, A., & Larsen, K. G. (2006). A tutorial on Uppaal 4.0. Aalborg, Denmark. URL: http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf.

  • Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. (2005). Comparison of the expressiveness of timed automata and time Petri nets. In Third International Conference, FORMATS 2005, Uppsala, Sweden, 26–28 September 2005 (pp. 211–225). Berlin Heidelberg: Springer. https://doi.org/10.1007/11603009_17.

  • Bollig, B., & Leucker, M. (2004). Message-passing automata are expressively equivalent to EMSO logic. In 15th International Conference CONCUR 2004—Concurrency Theory, London, UK, 31 August–3 September 2004 (pp. 146–160). Berlin Heidelberg: Springer. https://doi.org/10.1007/978-3-540-28644-8_10.

  • Chrobot, S., & Daszczuk, W. B. (2006). Communication dualism in distributed systems with Petri net interpretation. Theoretical and Applied Informatics, 18(4), 261–278. URL: https://taai.iitis.pl/taai/article/view/250/.

  • Clarke, E. M., Grumberg, O., & Peled, D. (1999). Model checking. Cambridge, MA: MIT Press. ISBN: 0-262-03270-8.

    MATH  Google Scholar 

  • Czejdo, B., Bhattacharya, S., Baszun, M., & Daszczuk, W. B. (2016). Improving resilience of autonomous moving platforms by real-time analysis of their cooperation. Autobusy-TEST, 17(6), 1294–1301. URL: http://www.autobusy-test.com.pl/images/stories/Do_pobrania/2016/nr%206/logistyka/10_l_czejdo_bhattacharya_baszun_daszczuk.pdf.

  • Daszczuk, W. B. (2000). State space reduction for reachability graph of CSM automata. ICS WUT Research Report No 10/2000. https://doi.org/10.13140/RG.2.2.17223.91047.

  • Daszczuk, W. B. (2001). Evaluation of temporal formulas based on “Checking By Spheres.” In Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4–6 September 2001 (pp. 158–164). IEEE. https://doi.org/10.1109/dsd.2001.952267.

  • Daszczuk, W. B. (2002). Critical trees: counterexamples in model checking of CSM systems using CBS algorithm. ICS WUT Research Report No. 8/2002. https://doi.org/10.13140/RG.2.2.13228.16003.

  • Daszczuk, W. B. (2003). Verification of temporal properties in concurrent systems. Warsaw University of Technology. URL: https://repo.pw.edu.pl/docstore/download/WEiTI-0b7425b5-2375-417b-b0fa-b1f61aed0623/Daszczuk.pdf.

  • Daszczuk, W. B. (2008). Deadlock and termination detection using IMDS formalism and model checking, Version 2. ICS WUT Research Report No. 2/2008. https://doi.org/10.13140/RG.2.2.23294.48969.

  • Daszczuk, W. B. (2017a). Communication and resource deadlock analysis using IMDS formalism and model checking. The Computer Journal, 60(5), 729–750. https://doi.org/10.1093/comjnl/bxw099.

  • Daszczuk, W. B. (2017b). Threefold analysis of distributed systems: IMDS, Petri net and distributed automata DA3. In 37th IEEE Software Engineering Workshop, Federated Conference on Computer Science and Information Systems, FEDCSIS’17, Prague, Czech Republic, 3–6 September 2017 (pp. 377–386). IEEE Comput. Soc. Press. https://doi.org/10.15439/2017f32.

  • Daszczuk, W. B. (2018a). Siphon-based deadlock detection in Integrated Model of Distributed Systems (IMDS). In Federated Conference on Computer Science and Information Systems, 3rd Workshop on Constraint Programming and Operation Research Applications (CPORA’18), Poznań, Poland, 9–12 September 2018 (pp. 421–431). IEEE. https://doi.org/10.15439/2018f114.

  • Daszczuk, W. B. (2018b). Specification and verification in integrated model of distributed systems (IMDS). MDPI Computers, 7(4), 1–26. https://doi.org/10.3390/computers7040065.

  • Daszczuk, W. B. (2019). Asynchronous specification of production cell benchmark in integrated model of distributed systems. In R. Bembenik, L. Skonieczny, G. Protaziuk, M. Kryszkiewicz, & H. Rybinski (Eds.), 23rd International Symposium on Methodologies for Intelligent Systems, ISMIS 2017, Studies in Big Data, Vol. 40, Warsaw, Poland, 26–29 June 2017 (pp. 115–129). Cham, Switzerland: Springer International Publishing. https://doi.org/10.1007/978-3-319-77604-0_9.

  • Daszczuk, W. B, & Mieścicki, J. (2001). JADE—A platform for research on cooperation of physical and virtual agents. ICS WUT Research Report No 15/2001.

    Google Scholar 

  • Daszczuk, W. B., & Zuberek, W. M. (2018). Deadlock detection in distributed systems using the IMDS formalism and Petri nets. In W. Zamojski, J. Mazurkiewicz, J. Sugier, T. Walkowiak, & J. Kacprzyk (Eds.), 12th International Conference on Dependability and Complex Systems, DepCoS-RELCOMEX 2017, Brunów, Poland, 2–6 July 2017. AISC (Vol. 582, pp. 118–130). Cham, Switzerland: Springer International Publishing. https://doi.org/10.1007/978-3-319-59415-6_12.

  • Daszczuk, W. B., Grabski, W., Wytrębowicz, J. (2001a). System modeling in the COSMA environment. In Proceedings Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4–6 September 2001 (pp. 152–157). Warsaw, Poland: IEEE Comput. Soc. https://doi.org/10.1109/dsd.2001.952264.

  • Daszczuk W B, Mieścicki J, Nowacki, M., & Wytrębowicz, J. (2001b). System level specification and verification using concurrent state machines and COSMA environment. In 8th International Conference on Mixed Design of Integrated Circuits and Systems, MIXDES’01, Zakopane, Poland, 21–23 June 2001 (pp. 525–532). arXiv:1703.05541.

  • Daszczuk, W. B., Mieścicki, J., Lewandowski, J., & Świrski, K. (1995). System for the integration of the block digital control system with the company network (in Polish: System Integracji Blokowego Cyfrowego Systemu Kontroli i Sterowania z Siecią Zakładową). In Problemy Badawcze Energetyki Cieplnej, Warszawa, 5–8 Grudnia 1995 (p. tom 1, 101–107). Warszawa: Oficyna Wydawnicza Politechniki Warszawskiej.

    Google Scholar 

  • Daszczuk, W. B., Bielecki, M., & Michalski, J. (2017). Rybu: Imperative-style preprocessor for verification of distributed systems in the Dedan environment. In KKIO’17—Software Engineering Conference, Rzeszów, Poland, 14–16 September 2017. Polish Information Processing Society. arXiv:1710.02722.

  • Daszczuk, W. B., Mieścicki, J., Kochan, A., Zając, K., Skurzak, K., & Duplicki, K. (1998a). A system for identification of fluidized bed furnace at the institute of heat engineering, WUT (In Polish: System identyfikacji paleniska fluidalnego w Instytucie Techniki Cieplnej PW). ICS WUT Research Report No 23/98. https://doi.org/10.13140/RG.2.2.14008.55049.

  • Daszczuk, W. B., Mieścicki, J., Krystosik, A., et al. (1998b). The organization of mobile computing systems using the GSM network as the communication subsystem. ICS WUT Technical Report No.15/1998.

    Google Scholar 

  • Dedan. (n.d.). URL: http://staff.ii.pw.edu.pl/dedan/files/DedAn.zip.

  • Fahland, D., Favre, C., Koehler, J., Lohmann, N., Völzer, H., & Wolf, K. (2011). Analysis on demand: Instantaneous soundness checking of industrial business process models. Data & Knowledge Engineering, 70(5), 448–466. https://doi.org/10.1016/j.datak.2011.01.004.

  • Grabski, W., Daszczuk, W. B., Mieścicki, J., & Dobrowolski, H. (1999). Verification of the event protocol for establishing and disconnecting a connection in the ESS system (in Polish: Weryfikacja zdarzeniowego protokołu nawiązywania i rozłączania połączenia w systemie ESS). ICS WUT Research Report No. 10/1999.

    Google Scholar 

  • Heiner, M, & Heisel, M. (1999). Modeling safety-critical systems with Z and Petri nets. In M. Felici, K. Kanoun, & A. Pasquini (Eds.), SAFECOMP ’99 Proceedings of the 18th International Conference on Computer Safety, Reliability and Security, Toulouse, France, 27–29 September 1999, LNCS (Vol. 1698, pp. 361–374). Berlin Heidelberg: Springer-Verlag. https://doi.org/10.1007/3-540-48249-0_31.

  • Heiner, M., Schwarick, M., & Wegener, J.-T. (2015). Charlie—An extensible Petri net analysis tool. In 36th International Conference, PETRI NETS 2015, Brussels, Belgium, 21–26 June 2015 (pp. 200–211). Cham, Switzerland: Springer International Publishing. https://doi.org/10.1007/978-3-319-19488-2_10.

  • Hoare, C. A. R. (1978). Communicating sequential processes. Communications of the ACM, 21(8), 666–677. https://doi.org/10.1145/359576.359585.

    Article  MATH  Google Scholar 

  • Holzmann, G. J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In 6th International Conference on Concurrency Theory, CONCUR’95, Philadelphia, PA, 21–24 August 1995 (pp. 453–455). Berlin Heidelberg: Springer-Verlag. https://doi.org/10.1007/3-540-60218-6_34.

  • Jia, W., & Zhou, W. (2005). Distributed network systems. From concepts to implementations. NETA 15, 513. New York: Springer. https://doi.org/10.1007/b102545.

  • Johnsen, E. B., Blanchette, J. C., Kyas, M., & Owe, O. (2009). Intra-object versus inter-object: Concurrency and reasoning in creol. Electronic Notes in Theoretical Computer Science, 243, 89–103. https://doi.org/10.1016/j.entcs.2009.07.007.

  • Kessler, C., & Keller, J. (2007). Models for parallel computing: Review and perspectives. In PARS-Mitteilungen, 13–29 December 2007 (pp. 13–29). URL: https://www.ida.liu.se/~chrke55/papers/modelsurvey.pdf.

  • Lee, G. M, Crespi, N., Choi, J. K., & Boussard, M. (2013). Internet of Things. In Evolution of Telecommunication Services, LNCS 7768 (pp. 257–282). Berlin Heidelberg: Springer-Verlag. https://doi.org/10.1007/978-3-642-41569-2_13.

  • Masticola, S. P, & Ryder, B. G. (1990). Static infinite wait anomaly detection in polynomial time. In 1990 International Conference on Parallel Processing, Urbana-Champaign, IL, 13–17 August 1990 (Vol. 2, pp. 78-87). University Park, PA: Pennsylvania State University Press. URL: https://rucore.libraries.rutgers.edu/rutgers-lib/57963/.

  • May, D. (1983). Occam. ACM SIGPLAN Notices, 18(4), 69–79. https://doi.org/10.1145/948176.948183.

    Article  Google Scholar 

  • Mieścicki, J. (2006). The use of model checking and the COSMA environment in the design of reactive systems. Annales UMCS, Informatica Vol. AI, 4AI, 244–253. http://dlibra.umcs.lublin.pl/dlibra/plain-content?id=17558.

  • Mieścicki, J., & Daszczuk, W. B. (2006). Behavioral and real-time verification of a pipeline in the COSMA environment. Annales UMCS, Informatica Vol. AI, 4AI, 254–265. https://journals.umcs.pl/ai/article/view/3061.

  • Mieścicki, J., Baszun, M., Daszczuk, W. B., & Czejdo, B. (1996). Verification of Concurrent Engineering Software Using CSM Models. In 2nd World Conference on Integrated Design and Process Technology, Austin, TX, 1–4 December 1996 (pp. 322–330). Dallas, TX: SDPS. arXiv:1704.06351.

  • Mieścicki, J., Dobrowolski, H., Daszczuk, W. B. (2003). Model checking of multi-agent system’s communication protocols specified using the Z notation. ICS WUT Research Report No. 17/2003.

    Google Scholar 

  • Mieścicki, J., Czejdo, B., Daszczuk, W. B. (2004). Model checking in the COSMA environment as a support for the design of pipelined processing. In European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyväskylä, Finland, 24–28 July 2004. Jyväskylä, Finland. arXiv:1705.04728.

  • Mieścicki, J., Daszczuk, W. B., … Adamiec, R. (1992). KURMAN: The system supporting the design of multidimensional automated control systems (in Polish KURMAN: System wspomagający projektowanie wielowymiarowych układów automatycznej regulacji). ICS WUT Research Report No 10/92.

    Google Scholar 

  • Mieścicki, J., Flisiak, D., Czuchaj, A., & Daszczuk, W. B. (1998). Specification and verification of SMS-based data stream protocol, ICS WUT Research Report No 16/98.

    Google Scholar 

  • Mieścicki, J., Kurman, K. J., & Daszczuk, W. B. (1995). MIKOZ: The method for identification and coordination of feedback interactions in the regulation of continuous technological processes (in Polish: MIKOZ: Metoda identyfikacji i koordynacji oddziaływań zwrotnych). ICS WUT Research Report No. 26/95.

    Google Scholar 

  • Milner, R. (1983). Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3), 267–310. https://doi.org/10.1016/0304-3975(83)90114-7.

    Article  MathSciNet  MATH  Google Scholar 

  • Milner, R. (1984). A calculus of communicating systems. Berlin: Springer-Verlag.

    MATH  Google Scholar 

  • Miller, S. P., Whalen, M. W., & Cofer, D. D. (2010). Software model checking takes off. Communications of the ACM, 53(2), 58–64. https://doi.org/10.1145/1646353.1646372.

    Article  Google Scholar 

  • Moy, Y., Ledinot, E., Delseny, H., & Monate, B. (2013). Testing or formal verification: DO-178C alternatives and industrial experience. IEEE Software, 30(3), 50–57. https://doi.org/10.1109/ms.2013.43.

  • NASA. (2007). NASA systems engineering handbook. NASA. URL: http://www.acq.osd.mil/se/docs/NASA-SP-2007-6105-Rev-1-Final-31Dec2007.pdf.

  • Popescu, C., & Martinez Lastra, J. L. (2010). Formal methods in factory automation. In J. Silvestre-Blanes (Ed.), Factory automation (pp. 463–475). Rijeka, Croatia: InTech. https://doi.org/10.5772/9526.

  • Reniers, M. A, & Willemse, T. A. C. (2011). Folk theorems on the correspondence between state-based and event-based systems. In 37th Conference on Current Trends in Theory and Practice of Computer Science, Nový Smokovec, Slovakia, 22–28 January 2011 (pp. 494–505). Berlin: Springer-Verlag. https://doi.org/10.1007/978-3-642-18381-2_41.

  • Rosa, N. S., & Cunha, P. R. F. (2004). A software architecture-based approach for formalising middleware behaviour. Electronic Notes in Theoretical Computer Science, 108, 39–51. https://doi.org/10.1016/j.entcs.2004.01.011.

    Article  Google Scholar 

  • Savoiu, N., Shukla, S. K., & Gupta, R. K. (2002). Automated concurrency re-assignment in high level system models for efficient system-level simulation. In Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, Paris, France, 4–8 March 2002 (pp. 875–881). IEEE Comput. Soc. https://doi.org/10.1109/date.2002.998404.

  • Schaefer, I., & Hahnle, R. (2011). Formal methods in software product line engineering. Computer, 44(2), 82–85. https://doi.org/10.1109/MC.2011.47.

    Article  Google Scholar 

  • Tai, K. (1994). Definitions and detection of deadlock, livelock, and starvation in concurrent programs. In D. P. Agrawal (Ed.), 1994 International Conference on Parallel Processing (ICPP’94), Raleigh, NC, 15–19 August 1994 (pp. 69–72). Boca Raton: CRC Press. https://doi.org/10.1109/icpp.1994.84.

  • van Glabbeek, R., Goltz, U., & Schicke, J.-W. (2008). On synchronous and asynchronous interaction in distributed systems. In 33rd International Symposium, MFCS 2008, Toruń, Poland, 25–29 August 2008 (pp. 16–35). Berlin Heidelberg: Springer. https://doi.org/10.1007/978-3-540-85238-4_2.

  • Zielonka, W. (1987). Notes on finite asynchronous automata. RAIRO—Theoretical Informatics and Applications, 21(2), 99–135. https://doi.org/10.1051/ita/1987210200991.

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Warsaw University of Technology, Warsaw, Poland

    Wiktor B. Daszczuk

Authors
  1. Wiktor B. Daszczuk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wiktor B. Daszczuk .

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Daszczuk, W.B. (2020). Introduction. In: Integrated Model of Distributed Systems. Studies in Computational Intelligence, vol 817. Springer, Cham. https://doi.org/10.1007/978-3-030-12835-7_1

Download citation

Publish with us

Policies and ethics

Search

Navigation