{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T04:36:27Z","timestamp":1760243787083,"version":"build-2065373602"},"reference-count":30,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2011,1,19]],"date-time":"2011-01-19T00:00:00Z","timestamp":1295395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>A current trend in the development and implementation of industrial applications is to use wireless networks to communicate the system nodes, mainly to increase application flexibility, reliability and portability, as well as to reduce the implementation cost. However, the nondeterministic and concurrent behavior of distributed systems makes their analysis and design complex, often resulting in less than satisfactory performance in simulation and test bed scenarios, which is caused by using imprecise models to analyze, validate and design these systems. Moreover, there are some simulation platforms that do not support these models. This paper presents a design and validation method forWireless Sensor and Actuator Networks (WSAN) which is supported on a minimal set of wireless components represented in Colored Petri Nets (CPN). In summary, the model presented allows users to verify the design properties and structural behavior of the system.<\/jats:p>","DOI":"10.3390\/s110101059","type":"journal-article","created":{"date-parts":[[2011,1,19]],"date-time":"2011-01-19T12:16:40Z","timestamp":1295439400000},"page":"1059-1077","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal Specification and Design Techniques for Wireless Sensor and Actuator Networks"],"prefix":"10.3390","volume":"11","author":[{"given":"Diego","family":"Mart\u00ednez","sequence":"first","affiliation":[{"name":"Department of Automation and Electronics, Autonomous University of the West, Cll 25 # 115 - 85 Km. 2 V\u00eda Cali-Jamund\u00ed, Colombia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6400-4164","authenticated-orcid":false,"given":"Apolinar","family":"Gonz\u00e1lez","sequence":"additional","affiliation":[{"name":"Faculty of Mechanical and Electrical Engineering, University of Colima, Av., Universidad # 333, 28000 Colima, Mexico"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francisco","family":"Blanes","sequence":"additional","affiliation":[{"name":"Department of Computer Engineering (DISCA), Polytechnic University of Valence, Camino de Vera s\/n, Valencia, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ra\u00fal","family":"Aquino","sequence":"additional","affiliation":[{"name":"Faculty of Mechanical and Electrical Engineering, University of Colima, Av., Universidad # 333, 28000 Colima, Mexico"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9","family":"Simo","sequence":"additional","affiliation":[{"name":"Department of Computer Engineering (DISCA), Polytechnic University of Valence, Camino de Vera s\/n, Valencia, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfons","family":"Crespo","sequence":"additional","affiliation":[{"name":"Department of Computer Engineering (DISCA), Polytechnic University of Valence, Camino de Vera s\/n, Valencia, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2011,1,19]]},"reference":[{"key":"ref_1","unstructured":"Mart\u00ednez, D., Balbastre, P., Blanes, F., Simo, J., and Crespo, A. (2009, January 27\u201328). Design of control applications on WSAN with mesh architecture. Albuquerque, NM, USA."},{"key":"ref_2","first-page":"95","article-title":"Procedimiento de diseno para minimizar el consumo de potencia y los retrasos en WSAN","volume":"7","author":"Balbastre","year":"2010","journal-title":"Revista Iberoamericana de Autom\u00f3tica e Inform\u00e1tica Industrial"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Hristu-Varsakelis, D., and Levine, W.S. (2005). Handbook of Networked and Embedded Control Systems, Springer.","DOI":"10.1007\/b137198"},{"key":"ref_4","unstructured":"Lee, S., Park, J.H., Ha, K.N., and Lee, K.C. (2008, January 21\u201323). Wireless networked control system using NDIS-based four-layer architecture for IEEE 802.11b. Dresden, Germany."},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Cena, I.G., Bertolotti, A.C., and Zunino, V.C. (2008, January 21\u201323). Industrial applications of IEEE 802.11e WLANs. Dresden, Germany.","DOI":"10.1109\/WFCS.2008.4638739"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Moraes, R., Portugal, P., Vasques, F., and Fonseca, J.A. (2008, January 21\u201323). Limitations of the IEEE 802.11e EDCA protocol when supporting real-time communication. Dresden, Germany.","DOI":"10.1109\/WFCS.2008.4638712"},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1109\/COMST.2007.4444752","article-title":"A survey on power control issues in wireless sensor networks","volume":"9","author":"Pantazis","year":"2007","journal-title":"IEEE Commun. Surv. Tutorials"},{"key":"ref_8","unstructured":"Zigbee Specification. Available online: http:\/\/www.Zigbee.org (accessed on 7 October 2010)."},{"key":"ref_9","unstructured":"Wireless HART. Available online: http:\/\/www.hartcomm2.org\/ (accessed on 30 September 2010)."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/s11241-008-9063-4","article-title":"TDBS: A time division beacon scheduling mechanism for ZigBee cluster-tree wireless sensor networks","volume":"40","author":"Cunha","year":"2008","journal-title":"Real-Time Syst. J"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Lennvall, T., Svensson, S., and Hekland, F (2008, January 21\u201323). A Comparison of WirelessHART and Zigbee for Industrial Applications. Dresden, Germany.","DOI":"10.1109\/WFCS.2008.4638746"},{"key":"ref_12","unstructured":"Saewong, S., and Rajkumar, R (2003, January 27\u201330). Practical voltage-scaling for fixed-priority RT-systems. Washington, DC, USA."},{"key":"ref_13","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1049\/sej.1993.0034","article-title":"Applying new scheduling theory to static priority pre-emptive scheduling","volume":"8","author":"Audsley","year":"1993","journal-title":"Software Eng. J"},{"key":"ref_14","unstructured":"Palencia, J.C., Guti\u00e9rrez, J.J., and Gonzalez, M. (1997, January 11\u201313). On the schedulability analysis for distributed hard real-time systems. Toledo, Spain."},{"key":"ref_15","unstructured":"Spuri, M (1996). Technic Report Inria-00073818, version 1,."},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/0165-6074(94)90080-9","article-title":"Holistic schedulability analysis for distributed hard real-time systems","volume":"40","author":"Tindell","year":"1994","journal-title":"Microproc. Microprog"},{"key":"ref_17","unstructured":"Tiny, O.S. Available online: http:\/\/www.tinyos.net\/. (accessed on 20 August 2010)."},{"key":"ref_18","unstructured":"Mejia-Alvarez, P., Levner, E., and Mosse, D. (2002, January 24\u201327). Power-optimized scheduling server for real-time tasks. San Jose, CA, USA."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1109\/TII.2006.890494","article-title":"Elastic DVS management in processors with discrete voltage\/frequency modes","volume":"3","author":"Marinoni","year":"2007","journal-title":"IEEE Trans. Ind. Inform"},{"key":"ref_20","unstructured":"Zhu, Y., and Mueller, F (2004, January 25\u201328). Feedback EDF scheduling exploiting dynamic voltage scaling. Toronto, Canada."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Pillai, P., and Shin, K.G. (2001, January 21\u201324). Real-time dynamic voltage scaling for low-power embedded operating systems. Banff, Canada.","DOI":"10.1145\/502034.502044"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Meshkova, E., Riihijarvi, J., Oldewurtel, F., Jardak, Ch., and Mahonen, P. (2008, January 11\u201313). Service-oriented design methodology for wireless sensor networks: A view through case studies. Taichung, Taiwan.","DOI":"10.1109\/SUTC.2008.43"},{"key":"ref_23","unstructured":"Bonivento, A., Sangiovanni-Vincentelli, A., Graziosi, F., and Santucci, F (2005, January 7). SERAN: A semi random protocol solution for clustered wireless sensor networks. Washintong, DC, USA."},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Bonivento, A., Carloni, L., and Sangiovanni-Vincentelli, A. (2006, January 6\u201310). Platform-based design of wireless sensor networks for industrial applications. Munich, Germany.","DOI":"10.1109\/DATE.2006.243975"},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Prasad, V., Yan, T., Jayachandran, P., Li, Z., Son, S., Stankovic, J., Hansson, J., and Abdelzaher, T (2007, January 3\u20136). ANDES: An analysis-based design tool for wireless sensor networks. Tucson, AZ, USA.","DOI":"10.1109\/RTSS.2007.28"},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"2157","DOI":"10.3390\/s7102157","article-title":"Wireless Sensor\/Actuator Network Design for Mobile Control Applications","volume":"10","author":"Xia","year":"2007","journal-title":"Sensors"},{"key":"ref_27","unstructured":"Varma, A., Debes, E., Kozintsev, I., and Jacob, B. (, January January). Instruction-level power dissipation in the intel XScale embedded microprocessor. San Jose, CA, USA."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/3-540-58043-3_21","article-title":"An introduction to the theoretical aspects of colored Petri Nets","volume":"803","author":"Bakker","year":"1994","journal-title":"A Decade of Concurrency, Lecture Notes in Computer Science"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Jensen, K. (1997, January 2\u20134). A brief introduction to Colored Petri Nets. Enschede, The Netherlands.","DOI":"10.1007\/BFb0035389"},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","article-title":"Colored Petri Nets and CPN tools for modelling and validation of concurrent systems","volume":"9","author":"Jensen","year":"2007","journal-title":"Int. J. Softw. Tools Technol. Transf"}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/11\/1\/1059\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T21:54:58Z","timestamp":1760219698000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/11\/1\/1059"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,19]]},"references-count":30,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2011,1]]}},"alternative-id":["s110101059"],"URL":"https:\/\/doi.org\/10.3390\/s110101059","relation":{},"ISSN":["1424-8220"],"issn-type":[{"type":"electronic","value":"1424-8220"}],"subject":[],"published":{"date-parts":[[2011,1,19]]}}}