{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T09:07:10Z","timestamp":1775293630786,"version":"3.50.1"},"reference-count":75,"publisher":"MDPI AG","issue":"4","license":[{"start":{"date-parts":[[2018,12,2]],"date-time":"2018-12-02T00:00:00Z","timestamp":1543708800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers"],"abstract":"<jats:p>Distributed systems, such as the Internet of Things (IoT) and cloud computing, are becoming popular. This requires modeling that reflects the natural characteristics of such systems: the locality of independent components, the autonomy of their decisions, and asynchronous communication. Automated verification of deadlocks and distributed termination supports rapid development. Existing techniques do not reflect some features of distribution. Most formalisms are synchronous and\/or use some kind of global state, both of which are unrealistic. No model supports the communication duality that allows the integration of a remote procedure call and client-server paradigm into a single, uniform model. The majority of model checkers refer to total deadlocks. Usually, they do not distinguish between communication deadlocks from resource deadlocks and deadlocks from distributed termination. Some verification mechanisms check partial deadlocks at the expense of restricting the structure of the system being verified. The paper presents an original formalism for the modeling and verification of distributed systems. The Integrated Model of Distributed Systems (IMDS) defines a distributed system as two sets: states and messages, and the relationship of the \u201cactions\u201d between these sets. Communication duality provides projections on servers and on traveling agents, but the uniform specification of the verified system is preserved. General temporal formulas over IMDS, independent of the structure of the verified system, allow automated verification. These formulas distinguish between deadlocks and distributed termination, and between communication deadlocks and resource deadlocks. Partial deadlocks and partial termination can be checked. The Dedan tool was developed using IMDS formalism.<\/jats:p>","DOI":"10.3390\/computers7040065","type":"journal-article","created":{"date-parts":[[2018,12,3]],"date-time":"2018-12-03T06:02:09Z","timestamp":1543816929000},"page":"65","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Specification and Verification in Integrated Model of Distributed Systems (IMDS)"],"prefix":"10.3390","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7532-362X","authenticated-orcid":false,"given":"Wiktor B.","family":"Daszczuk","sequence":"first","affiliation":[{"name":"Institute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15\/19, 00-665 Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2018,12,2]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1109\/MC.2011.47","article-title":"Formal Methods in Software Product Line Engineering","volume":"44","author":"Schaefer","year":"2011","journal-title":"Computer"},{"key":"ref_2","first-page":"244","article-title":"The use of model checking and the COSMA environment in the design of reactive systems","volume":"4","year":"2006","journal-title":"Ann. UMCS Inform."},{"key":"ref_3","unstructured":"Mie\u015bcicki, J., Baszun, M., Daszczuk, W.B., and Czejdo, B. (1996, January 1\u20134). Verification of Concurrent Engineering Software Using CSM Models. Proceedings of the 2nd World Conference on Integrated Design and Process Technology, Austin, TX, USA."},{"key":"ref_4","unstructured":"Daszczuk, W.B. (2001, January 4\u20136). Evaluation of temporal formulas based on \u201cChecking By Spheres\u201d. Proceedings of the Euromicro Symposium on Digital Systems Design, Warsaw, Poland."},{"key":"ref_5","unstructured":"Daszczuk, W.B., Grabski, W., Mie\u015bcicki, J., and Wytr\u0119bowicz, J. (2001, January 4\u20136). System modeling in the COSMA environment. Proceedings of the Euromicro Symposium on Digital Systems Design, Warsaw, Poland."},{"key":"ref_6","unstructured":"Daszczuk, W.B., Mie\u015bcicki, J., Nowacki, M., and Wytr\u0119bowicz, J. (2001, January 21\u201323). System Level Specification and Verification Using Concurrent State Machines and COSMA Environment. Proceedings of the 8th International Conference on Mixed Design of Integrated Circuits and Systems (MIXDES\u201901), Zakopane, Poland."},{"key":"ref_7","unstructured":"Mie\u015bcicki, J., Czejdo, B., and Daszczuk, W.B. (2004, January 24\u201328). Model Checking in the COSMA Environment as a Support for the Design of Pipelined Processing. Proceedings of the European Congress on Computational Methods in Applied Sciences and Engineering (ECCOMAS 2004), Jyv\u00e4skyl\u00e4, Finland."},{"key":"ref_8","first-page":"254","article-title":"Behavioral and real-time verification of a pipeline in the COSMA environment","volume":"4","author":"Daszczuk","year":"2006","journal-title":"Ann. UMCS Inform."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Lee, G.M., Crespi, N., Choi, J.K., and Boussard, M. (2013). Internet of Things. Evolution of Telecommunication Services, Springer. LNCS 7768.","DOI":"10.1007\/978-3-642-41569-2_13"},{"key":"ref_10","first-page":"261","article-title":"Communication Dualism in Distributed Systems with Petri Net Interpretation","volume":"18","author":"Chrobot","year":"2006","journal-title":"Theor. Appl. Inform."},{"key":"ref_11","first-page":"729","article-title":"Communication and Resource Deadlock Analysis using IMDS Formalism and Model Checking","volume":"60","author":"Daszczuk","year":"2017","journal-title":"Comput. J."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Reniers, M.A., and Willemse, T.A.C. (2011, January 22\u201328). Folk Theorems on the Correspondence between State-Based and Event-Based Systems. Proceedings of the 37th Conference on Current Trends in Theory and Practice of Computer Science, Nov\u00fd Smokovec, Slovakia.","DOI":"10.1007\/978-3-642-18381-2_41"},{"key":"ref_13","unstructured":"Jia, W., and Zhou, W. (2005). Distributed Network Systems: From Concepts to Implementations, Springer."},{"key":"ref_14","unstructured":"Kessler, C., and Keller, J. (2007). Models for Parallel Computing: Review and Perspectives. PARS-Mitteilungen, Gesellschaft f\u00fcr Informatik."},{"key":"ref_15","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","article-title":"Calculi for synchrony and asynchrony","volume":"25","author":"Milner","year":"1983","journal-title":"Theor. Comput. Sci."},{"key":"ref_16","unstructured":"Savoiu, N., Shukla, S.K., and Gupta, R.K. (2002, January 4\u20138). Automated concurrency re-assignment in high level system models for efficient system-level simulation. Proceedings of the 2002 Design, Automation and Test in Europe Conference and Exhibition, Paris, France."},{"key":"ref_17","unstructured":"van Glabbeek, R., Goltz, U., and Schicke, J.-W. (2008, January 25\u201329). On Synchronous and Asynchronous Interaction in Distributed Systems. Proceedings of the 33rd International Symposium (MFCS 2008), Toru\u0144, Poland."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.entcs.2004.01.011","article-title":"A Software Architecture-Based Approach for Formalising Middleware Behaviour","volume":"108","author":"Rosa","year":"2004","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J. (1995, January 21\u201324). Tutorial: Proving properties of concurrent systems with SPIN. Proceedings of the 6th International Conference on Concurrency Theory (CONCUR\u201995), Philadelphia, PA, USA.","DOI":"10.1007\/3-540-60218-6_34"},{"key":"ref_20","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D. (1999). Model Checking, MIT Press."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1051\/ita\/1987210200991","article-title":"Notes on finite asynchronous automata","volume":"21","author":"Zielonka","year":"1987","journal-title":"RAIRO Theor. Inform. Appl. Inform. Th\u00e9or. Appl."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor. Comput. Sci."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoare","year":"1978","journal-title":"Commun. ACM"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1002\/spe.1006","article-title":"Developing UPPAAL over 15 years","volume":"41","author":"Behrmann","year":"2011","journal-title":"Softw. Pract. Exp."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Milner, R. (1984). A Calculus of Communicating Systems, Springer.","DOI":"10.1007\/3-540-15670-4_10"},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/948176.948183","article-title":"OCCAM","volume":"18","author":"May","year":"1983","journal-title":"ACM SIGPLAN Not."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/j.entcs.2009.07.007","article-title":"Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol","volume":"243","author":"Johnsen","year":"2009","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Bollig, B., and Leucker, M. (September, January 31). Message-Passing Automata Are Expressively Equivalent to EMSO Logic. Proceedings of the 15th International Conference CONCUR 2004\u2014Concurrency Theory, London, UK.","DOI":"10.1007\/978-3-540-28644-8_10"},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"59","DOI":"10.4204\/EPTCS.3.5","article-title":"Serializing the Parallelism in Parallel Communicating Pushdown Automata Systems","volume":"3","author":"Balan","year":"2009","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"ref_30","unstructured":"Sandhu, K.K. (1992). Specification and description language (SDL). IEE Tutorial Colloquium on Formal Methods and Notations Applicable to Telecommunications, IET."},{"key":"ref_31","unstructured":"Broy, M., Fox, J., H\u00f6lzl, F., Koss, D., Kuhrmann, M., Meisinger, M., Penzenstadler, B., Rittmann, S., Sch\u00e4tz, B., and Spichkova, M. (2007). Service-Oriented Modeling of CoCoME with Focus and AutoFocus. The Common Component Modeling Example, Shaker."},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","article-title":"The model checker SPIN","volume":"23","author":"Holzmann","year":"1997","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Liu, Y., and Jiang, J. (2016, January 8\u201312). Analysis and Modeling for Interaction with Mobility Based on Pi-Calculus. Proceedings of the 2016 IEEE 14th International Conference on Dependable, Autonomic and Secure Computing, 14th International Conference on Pervasive Intelligence and Computing and 2nd International Conference on Big Data Intelligence and Computing and Cyber Science and Technology Congress (DASC\/PiCom\/DataCom\/CyberSciTech), Auckland, New Zealand.","DOI":"10.1109\/DASC-PICom-DataCom-CyberSciTec.2016.42"},{"key":"ref_34","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1109\/MS.2013.43","article-title":"Testing or Formal Verification: DO-178C Alternatives and Industrial Experience","volume":"30","author":"Moy","year":"2013","journal-title":"IEEE Softw."},{"key":"ref_35","unstructured":"Hirshorn, S.R. (2007). NASA Systems Engineering Handbook, NASA."},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/1646353.1646372","article-title":"Software model checking takes off","volume":"53","author":"Miller","year":"2010","journal-title":"Commun. ACM"},{"key":"ref_37","doi-asserted-by":"crossref","first-page":"448","DOI":"10.1016\/j.datak.2011.01.004","article-title":"Analysis on demand: Instantaneous soundness checking of industrial business process models","volume":"70","author":"Fahland","year":"2011","journal-title":"Data Knowl. Eng."},{"key":"ref_38","unstructured":"Huang, S.-T. (1989, January 5\u20139). Detecting termination of distributed computations by external agents. Proceedings of the 9th International Conference on Distributed Computing Systems, Newport Beach, CA, USA."},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/MC.1980.1653786","article-title":"The Deadlock Problem: An Overview","volume":"13","author":"Isloor","year":"1980","journal-title":"Computer"},{"key":"ref_40","unstructured":"Puhakka, A., and Valmari, A. (2000, January 21\u201325). Livelocks, Fairness and Protocol Verification. Proceedings of the 16th World Conference on Software: Theory and Practice, Beijing, China."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","article-title":"Model checking JAVA programs using JAVA PathFinder","volume":"2","author":"Havelund","year":"2000","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_42","unstructured":"Arcaini, P., Gargantini, A., and Riccobene, E. (2018, October 24). AsmetaSMV: A model checker for AsmetaL models\u2014Tutorial. Available online: https:\/\/air.unimi.it\/retrieve\/handle\/2434\/69105\/96882\/Tutorial_AsmetaSMV.pdf."},{"key":"ref_43","unstructured":"Sharma, N.K., and Bhargava, B. (1987). A Robust Distributed Termination Detection Algorithm, Purdue University Press. Available online: http:\/\/docs.lib.purdue.edu\/cgi\/viewcontent.cgi?article=1626&context=cstech."},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1145\/307988.307989","article-title":"Formal verification in hardware design: A survey","volume":"4","author":"Kern","year":"1999","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"ref_45","unstructured":"Ma, G. (2007). Model Checking Support for CoreASM: Model Checking Distributed Abstract State Machines Using Spin. [Master\u2019s Thesis, Simon Fraser University]."},{"key":"ref_46","unstructured":"Yang, Y., Chen, X., and Gopalakrishnan, G. (2008). Inspect: A Runtime Model Checker for Multithreaded C Programs, University of Utah. Report UUCS-08-004."},{"key":"ref_47","first-page":"1","article-title":"Synthesis of large dynamic concurrent programs from dynamic specifications","volume":"47","author":"Attie","year":"2016","journal-title":"Form. Methods Syst. Des."},{"key":"ref_48","unstructured":"Baier, C., and Katoen, J.-P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_49","unstructured":"Joosten, S.J.C., Julien, F.V., and Schmaltz, J. (2014, January 20). WickedXmas: Designing and Verifying on-chip Communication Fabrics. Proceedings of the 3rd International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS\u201914), Lausanne, Switzerland."},{"key":"ref_50","unstructured":"Martens, M. (2009). Establishing Properties of Interaction Systems. [PhD. Thesis, University of Mannheim]."},{"key":"ref_51","first-page":"426","article-title":"A Literature Review of Deadlock Prevention Policy Based on Petri Nets for Automated Manufacturing Systems","volume":"6","author":"Guan","year":"2012","journal-title":"Int. J. Digit. Content Technol. Its Appl."},{"key":"ref_52","first-page":"1294","article-title":"Improving Resilience of Autonomous Moving Platforms by real-time analysis of their Cooperation","volume":"17","author":"Czejdo","year":"2016","journal-title":"Autobusy-TEST"},{"key":"ref_53","first-page":"115","article-title":"Asynchronous Specification of Production Cell Benchmark in Integrated Model of Distributed Systems","volume":"Volume 40","author":"Bembenik","year":"2019","journal-title":"Studies in Big Data: 23rd International Symposium on Methodologies for Intelligent Systems (ISMIS 2017), Warsaw, Poland, 26\u201329 June 2017"},{"key":"ref_54","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/FI-2000-43123413","article-title":"Improving Partial Order Reductions for Universal Branching Time Properties","volume":"43","author":"Penczek","year":"2000","journal-title":"Fundam. Inform."},{"key":"ref_55","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/214451.214456","article-title":"Distributed snapshots: Determining global states of distributed systems","volume":"3","author":"Chandy","year":"1985","journal-title":"ACM Trans. Comput. Syst."},{"key":"ref_56","doi-asserted-by":"crossref","unstructured":"Dick, G., and Yao, X. (2014, January 6\u201311). Model representation and cooperative coevolution for finite-state machine evolution. Proceedings of the 2014 IEEE Congress on Evolutionary Computation (CEC), Beijing, China.","DOI":"10.1109\/CEC.2014.6900622"},{"key":"ref_57","doi-asserted-by":"crossref","unstructured":"Daszczuk, W.B. (2017, January 3\u20136). Threefold Analysis of Distributed Systems: IMDS, Petri Net and Distributed Automata DA3. Proceedings of the 37th IEEE Software Engineering Workshop, Federated Conference on Computer Science and Information Systems (FEDCSIS\u201917), Prague, Czech Republic.","DOI":"10.15439\/2017F32"},{"key":"ref_58","unstructured":"Daszczuk, W.B., Bielecki, M., and Michalski, J. (2017, January 14\u201316). Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment. Proceedings of the KKIO\u201917\u2014Software Engineering Conference, Rzesz\u00f3w, Poland."},{"key":"ref_59","unstructured":"Agrawal, D.P. (1994). Definitions and Detection of Deadlock, Livelock, and Starvation in Concurrent Programs. 1994 International Conference on Parallel Processing (ICPP\u201994), Raleigh, NC, 15\u201319 August 1994, CRC Press."},{"key":"ref_60","unstructured":"Masticola, S.P., and Ryder, B.G. (1990, January 13\u201317). Static Infinite Wait Anomaly Detection in Polynomial Time. Proceedings of the 1990 International Conference on Parallel Processing, Urbana-Champaign, IL, USA."},{"key":"ref_61","unstructured":"(2018, October 24). Dedan. Available online: http:\/\/staff.ii.pw.edu.pl\/dedan\/files\/DedAn.zip."},{"key":"ref_62","first-page":"135","article-title":"Fairness in Temporal Verification of Distributed Systems","volume":"Volume 761","author":"Zamojski","year":"2018","journal-title":"13th International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, Brun\u00f3w, Poland, 2\u20136 July 2018"},{"key":"ref_63","first-page":"359","article-title":"NuSMV 2: An OpenSource Tool for Symbolic Model Checking","volume":"Volume 2404","author":"Brinksma","year":"2002","journal-title":"CAV 2002: Computer Aided Verification, Copenhagen, Denmark, 27\u201331 July 2002"},{"key":"ref_64","first-page":"437","article-title":"The complexity of temporal logic model checking","volume":"Volume 4","author":"Balbiani","year":"2003","journal-title":"4th Conference Advances in Modal Logic (AiML\u20192002), Toulouse, France, 30 September\u20142 October 2004"},{"key":"ref_65","unstructured":"(2018, October 24). Dedan Examples. Available online: http:\/\/staff.ii.pw.edu.pl\/dedan\/files\/examples.zip."},{"key":"ref_66","doi-asserted-by":"crossref","unstructured":"Lewerentz, C., and Lindner, T. (1995). Formal Development of Reactive Systems; LNCS 891, Springer.","DOI":"10.1007\/3-540-58867-1"},{"key":"ref_67","first-page":"118","article-title":"Deadlock Detection in Distributed Systems Using the IMDS Formalism and Petri Nets","volume":"Volume 582","author":"Zamojski","year":"2018","journal-title":"12th International Conference on Dependability and Complex Systems, DepCoS-RELCOMEX 2017, Brun\u00f3w, Poland, 2\u20136 July 2017"},{"key":"ref_68","doi-asserted-by":"crossref","unstructured":"Daszczuk, W.B. (2018, January 9\u201312). Siphon-based deadlock detection in Integrated Model of Distributed Systems (IMDS). Proceedings of the Federated Conference on Computer Science and Information Systems, 3rd Workshop on Constraint Programming and Operation Research Applications (CPORA\u201918), Pozna\u0144, Poland.","DOI":"10.15439\/2018F114"},{"key":"ref_69","first-page":"361","article-title":"Modeling Safety-Critical Systems with Z and Petri Nets","volume":"Volume 1698","author":"Felici","year":"1999","journal-title":"SAFECOMP \u201999 Proceedings of the 18th International Conference on Computer Safety, Reliability and Security, Toulouse, France, 27\u201329 September 1999"},{"key":"ref_70","doi-asserted-by":"crossref","unstructured":"Heiner, M., Schwarick, M., and Wegener, J.-T. (2015, January 21\u201326). Charlie\u2014An Extensible Petri Net Analysis Tool. Proceedings of the 36th International Conference, PETRI NETS 2015, Brussels, Belgium.","DOI":"10.1007\/978-3-319-19488-2_10"},{"key":"ref_71","doi-asserted-by":"crossref","unstructured":"B\u00e9rard, B., Cassez, F., Haddad, S., Lime, D., and Roux, O.H. (2005, January 26\u201328). Comparison of the Expressiveness of Timed Automata and Time Petri Nets. Proceedings of the Third International Conference, FORMATS 2005, Uppsala, Sweden.","DOI":"10.1007\/11603009_17"},{"key":"ref_72","doi-asserted-by":"crossref","unstructured":"Silvestre-Blanes, J. (2010). Formal Methods in Factory Automation. Factory Automation, InTech.","DOI":"10.5772\/231"},{"key":"ref_73","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF01386390","article-title":"A note on two problems in connexion with graphs","volume":"1","author":"Dijkstra","year":"1959","journal-title":"Numer. Math."},{"key":"ref_74","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S0218126698000043","article-title":"The Application of Petri Nets to Workflow Management","volume":"8","year":"1998","journal-title":"J. Circuits Syst. Comput."},{"key":"ref_75","unstructured":"Kwiatkowska, M., Norman, G., and Parker, D. (2011, January 14\u201320). PRISM 4.0: Verification of Probabilistic Real-Time Systems. Proceedings of the 23rd International Conference, CAV 2011, Snowbird, UT, USA."}],"container-title":["Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-431X\/7\/4\/65\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T08:21:55Z","timestamp":1775290915000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-431X\/7\/4\/65"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,2]]},"references-count":75,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2018,12]]}},"alternative-id":["computers7040065"],"URL":"https:\/\/doi.org\/10.3390\/computers7040065","relation":{},"ISSN":["2073-431X"],"issn-type":[{"value":"2073-431X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,2]]}}}