{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T03:28:54Z","timestamp":1760239734002,"version":"build-2065373602"},"reference-count":57,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2020,12,26]],"date-time":"2020-12-26T00:00:00Z","timestamp":1608940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100009887","name":"Regione Siciliana","doi-asserted-by":"publisher","award":["08PA000PA90190"],"award-info":[{"award-number":["08PA000PA90190"]}],"id":[{"id":"10.13039\/501100009887","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>We propose a methodology to verify applications developed following programming patterns inspired by natural language that interact with physical environments and run on resource-constrained interconnected devices. Natural language patterns allow for the reduction of intermediate abstraction layers to map physical domain concepts into executable code avoiding the recourse to ontologies, which would need to be shared, kept up to date, and synchronized across a set of devices. Moreover, the computational paradigm we use for effective distributed execution of symbolic code on resource-constrained devices encourages the adoption of such patterns. The methodology is supported by a rule-based system that permits runtime verification of Software Under Test (SUT) on board the target devices through automated oracle and test case generation. Moreover, verification extends from syntactic and semantic checks to the evaluation of the effects of SUT execution on target hardware. Additionally, by exploiting rules tying sensors and actuators to physical quantities, the effects of code execution on the physical environment can be verified. The system is also able to build test code to highlight software issues that may arise during repeated SUT execution on the target hardware.<\/jats:p>","DOI":"10.3390\/s21010107","type":"journal-article","created":{"date-parts":[[2020,12,27]],"date-time":"2020-12-27T20:52:21Z","timestamp":1609102341000},"page":"107","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Knowledge-Based Verification of Concatenative Programming Patterns Inspired by Natural Language for Resource-Constrained Embedded Devices"],"prefix":"10.3390","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5480-2100","authenticated-orcid":false,"given":"Salvatore","family":"Gaglio","sequence":"first","affiliation":[{"name":"Department of Engineering, University of Palermo, Viale delle Scienze, Ed.6, 90128 Palermo, Italy"},{"name":"Institute for High Performance Computing and Networking (ICAR), National Research Council (CNR), Via Ugo La Malfa, 153, 90146 Palermo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8217-2230","authenticated-orcid":false,"given":"Giuseppe","family":"Lo Re","sequence":"additional","affiliation":[{"name":"Department of Engineering, University of Palermo, Viale delle Scienze, Ed.6, 90128 Palermo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1355-2969","authenticated-orcid":false,"given":"Gloria","family":"Martorella","sequence":"additional","affiliation":[{"name":"Department of Engineering, University of Palermo, Viale delle Scienze, Ed.6, 90128 Palermo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8763-7199","authenticated-orcid":false,"given":"Daniele","family":"Peri","sequence":"additional","affiliation":[{"name":"Department of Engineering, University of Palermo, Viale delle Scienze, Ed.6, 90128 Palermo, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2020,12,26]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1109\/JSYST.2014.2322503","article-title":"Design Techniques and Applications of Cyberphysical Systems: A Survey","volume":"9","author":"Khaitan","year":"2015","journal-title":"IEEE Syst. J."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1016\/j.jss.2015.01.027","article-title":"Enabling High-Level Application Development for the Internet of Things","volume":"103","author":"Patel","year":"2015","journal-title":"J. Syst. Softw."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Brouwers, N., Langendoen, K., and Corke, P. (2009, January 4\u20136). Darjeeling, a Feature-rich VM for the Resource Poor. Proceedings of the SenSys \u201909 7th ACM Conference on Embedded Networked Sensor Systems, Berkeley, CA, USA.","DOI":"10.1145\/1644038.1644056"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Cameron, C., Harvey, P., and Sventek, J. (2013, January 11\u201313). A Virtual Machine for the Insense Language. Proceedings of the 2013 International Conference on MOBILe Wireless MiddleWARE, Operating Systems, and Applications, Bologna, Italy.","DOI":"10.1109\/Mobilware.2013.17"},{"key":"ref_5","unstructured":"Korsholm, S. (2013, January 9\u201311). Flash Memory in Embedded Java Programs. Proceedings of the JTRES \u201911 9th International Workshop on Java Technologies for Real-Time and Embedded Systems, Karlsruhe, Germany."},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Aslam, F., Fennell, L., Schindelhauer, C., Ernst, P.T.G., Haussmann, E.S., and R\u00fchrup, Z.A.U. (2010, January 21\u201323). Optimized Java Binary and Virtual Machine for Tiny Motes. Proceedings of the 6th IEEE International Conference, DCOSS 2010, Santa Barbara, CA, USA.","DOI":"10.1007\/978-3-642-13651-1_2"},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Zheng, X., and Julien, C. (2015, January 17). Verification and Validation in Cyber Physical Systems: Research Challenges and a Way Forward. Proceedings of the SEsCPS \u201915 First International Workshop on Software Engineering for Smart Cyber-Physical Systems, Florence, Italy.","DOI":"10.1109\/SEsCPS.2015.11"},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2903144","article-title":"A Comparative Study of Recent Wireless Sensor Network Simulators","volume":"12","author":"Minakov","year":"2016","journal-title":"ACM Trans. Sen. Netw."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Iyenghar, P., Pulvermueller, E., Spieker, M., Wuebbelmann, J., and Westerkamp, C. (2013, January 29\u201331). Time and Memory-aware Runtime Monitoring for Executing Model-Based Test Cases in Embedded Systems. Proceedings of the 2013 11th IEEE International Conference on Industrial Informatics (INDIN), Bochum, Germany.","DOI":"10.1109\/INDIN.2013.6622936"},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2994595","article-title":"From Clarity to Efficiency for Distributed Algorithms","volume":"39","author":"Liu","year":"2017","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Araujo, W., Briand, L.C., and Labiche, Y. (2011, January 21\u201328). Enabling the Runtime Assertion Checking of Concurrent Contracts for the Java Modeling Language. Proceedings of the 2011 33rd International Conference on Software Engineering (ICSE), Honolulu, HI, USA.","DOI":"10.1145\/1985793.1985903"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.jss.2013.10.056","article-title":"Using SPIN for Automated Debugging of Infinite Executions of Java Programs","volume":"90","author":"Adalid","year":"2014","journal-title":"J. Syst. Softw."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Li, N., and Offutt, J. (April, January 31). An Empirical Analysis of Test Oracle Strategies for Model-Based Testing. Proceedings of the 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation, Cleveland, OH, USA.","DOI":"10.1109\/ICST.2014.49"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"2034","DOI":"10.1016\/j.jss.2008.02.047","article-title":"Bytecode Fault Injection for Java Software","volume":"81","author":"Ghosh","year":"2008","journal-title":"J. Syst. Softw."},{"key":"ref_15","first-page":"204","article-title":"A Semantic Approach for Automated Test Oracle Generation","volume":"45","author":"Guo","year":"2016","journal-title":"Comput. Lang. Syst. Struct."},{"key":"ref_16","unstructured":"Hasanain, W., Labiche, Y., and Gheorghe, S. (2015, January 9\u201311). Automated State-based Online Testing Real-time Embedded Software with RTEdge. Proceedings of the 2015 3rd International Conference on Model-Driven Engineering and Software Development (MODELSWARD), Loire Valley, France."},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s10270-013-0328-6","article-title":"Environment Modeling and Simulation for Automated Testing of Soft Real-time Embedded Software","volume":"14","author":"Iqbal","year":"2015","journal-title":"Softw. Syst. Model."},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/j.jss.2013.10.041","article-title":"An Approach to Testing Commercial Embedded Systems","volume":"88","author":"Yu","year":"2014","journal-title":"J. Syst. Softw."},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Iyenghar, P., Westerkamp, C., Wuebbelmann, J., and Pulvermueller, E. (2010, January 14\u201316). An Architecture for Deploying Model Based Testing in Embedded Systems. Proceedings of the 2010 Forum on Specification Design Languages (FDL 2010), Southampton, UK.","DOI":"10.1049\/ic.2010.0153"},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Darvas, D., Vi\u00f1uela, E.B., and Majzik, I. (2016, January 19\u201321). PLC Code Generation based on a Formal Specification Language. Proceedings of the 2016 IEEE 14th International Conference on Industrial Informatics (INDIN), Poitiers, France.","DOI":"10.1109\/INDIN.2016.7819191"},{"key":"ref_21","unstructured":"Adiego, B.F., Darvas, D., Tournier, J.C., Vi\u00f1uela, E.B., Blech, J.O., and Gonz\u00e1lez Su\u00e1, V. (2014). Automated Generation of Formal Models from ST Control Programs for Verification Purposes, CERN. CERN-ACC-NOTE-2014-0037."},{"key":"ref_22","unstructured":"Ur, B., McManus, E., Pak Yong Ho, M., and Littman, M.L. (May, January 26). Practical Trigger-action Programming in the Smart Home. Proceedings of the CHI \u201914 SIGCHI Conference on Human Factors in Computing Systems, Toronto, ON, Canada."},{"key":"ref_23","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1016\/j.future.2016.10.026","article-title":"Major Requirements for Building Smart Homes in Smart Cities based on Internet of Things Technologies","volume":"76","author":"Hui","year":"2017","journal-title":"Future Gener. Comput. Syst."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"735","DOI":"10.1109\/JIOT.2016.2554146","article-title":"An Internet-of-Things Enabled Connected Navigation System for Urban Bus Riders","volume":"3","author":"Handte","year":"2016","journal-title":"IEEE Internet Things J."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/j.future.2017.03.034","article-title":"Smart City and IoT","volume":"76","author":"Kim","year":"2017","journal-title":"Future Gener. Comput. Syst."},{"key":"ref_26","first-page":"1","article-title":"Intelligent Personal Assistants Based on Internet of Things Approaches","volume":"12","author":"Santos","year":"2017","journal-title":"IEEE Syst. J."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1109\/JIOT.2017.2664072","article-title":"Structural Health Monitoring Framework Based on Internet of Things: A Survey","volume":"4","author":"Tokognon","year":"2017","journal-title":"IEEE Internet Things J."},{"key":"ref_28","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1145\/635506.605407","article-title":"Mat\u00c9: A Tiny Virtual Machine for Sensor Networks","volume":"30","author":"Levis","year":"2002","journal-title":"SIGARCH Comput. Archit. News"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Alessandrelli, D., Petracca, M., and Pagano, P. (2013, January 20\u201323). T-Res: Enabling Reconfigurable In-network Processing in IoT-based WSNs. Proceedings of the 2013 IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS), Cambridge, MA, USA.","DOI":"10.1109\/DCOSS.2013.75"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Bocchino, S., Fedor, S., and Petracca, M. (2015). PyFUNS: A Python Framework for Ubiquitous Networked Sensors. Wireless Sensor Networks, Springer.","DOI":"10.1007\/978-3-319-15582-1_1"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3105923","article-title":"DC4CD: A Platform for Distributed Computing on Constrained Devices","volume":"17","author":"Gaglio","year":"2017","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Kauling, D., and Mahmoud, Q.H. (2017, January 8\u201311). Sensorian Hub: An IFTTT-based Platform for Collecting and Processing Sensor Data. Proceedings of the 2017 14th IEEE Annual Consumer Communications Networking Conference (CCNC), Vegas, NV, USA.","DOI":"10.1109\/CCNC.2017.7983159"},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Campagna, G., Ramesh, R., Xu, S., Fischer, M., and Lam, M.S. (2017, January 3\u20137). Almond: The Architecture of an Open, Crowdsourced, Privacy-Preserving, Programmable Virtual Assistant. Proceedings of the WWW \u201917 26th International Conference on World Wide Web, Perth, Australia.","DOI":"10.1145\/3038912.3052562"},{"key":"ref_34","doi-asserted-by":"crossref","unstructured":"Harrand, N., Fleurey, F., Morin, B., and Husa, K.E. (2016, January 2\u20137). ThingML: A Language and Code Generation Framework for Heterogeneous Targets. Proceedings of the MODELS \u201916 ACM\/IEEE 19th International Conference on Model Driven Engineering Languages and Systems, Saint-Malo, France.","DOI":"10.1145\/2976767.2976812"},{"key":"ref_35","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/s10270-013-0330-z","article-title":"Formal verification and validation of embedded systems: The UML-based MADES approach","volume":"14","author":"Baresi","year":"2015","journal-title":"Softw. Syst. Model."},{"key":"ref_36","first-page":"1","article-title":"High-Level Design of Wireless Sensor Networks for Performance Optimization Under Security Hazards","volume":"13","author":"Posadas","year":"2017","journal-title":"ACM Trans. Sen. Netw."},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Berger, C. (2014). SenseDSL: Automating the Integration of Sensors for MCU-Based Robots and Cyber-Physical Systems. Proceedings of the DSM \u201914 14th Workshop on Domain-Specific Modeling, ACM.","DOI":"10.1145\/2688447.2688455"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Mamun, M.A.A., Berger, C., and Hansson, J. (2013, January 27). MDE-based Sensor Management and Verification for a Self-driving Miniature Vehicle. Proceedings of the DSM \u201913 2013 ACM Workshop on Domain-Specific Modeling, Indianapolis, IN, USA.","DOI":"10.1145\/2541928.2541929"},{"key":"ref_39","first-page":"102","article-title":"Domain-specific Languages in Prolog for Declarative Expert Knowledge in Rules and Ontologies","volume":"51","author":"Seipel","year":"2018","journal-title":"Comput. Lang. Syst. Struct."},{"key":"ref_40","unstructured":"Drawel, N., Qu, H., Bentahar, J., and Shakshuki, E. (2018). Specification and Automatic Verification of Trust-based Multi-Agent Systems. Future Gener. Comput. Syst."},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1016\/j.future.2015.09.013","article-title":"Logic-based Modeling of Information Transfer in Cyber-Physical Multi-Agent Systems","volume":"56","year":"2016","journal-title":"Future Gener. Comput. Syst."},{"key":"ref_42","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3232616","article-title":"Maintenance of Smart Buildings Using Fault Trees","volume":"14","author":"Cauchi","year":"2018","journal-title":"ACM Trans. Sen. Netw."},{"key":"ref_43","doi-asserted-by":"crossref","unstructured":"Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., and Tillmann, N. (2010, January 1\u20134). Copilot: A Hard Real-Time Runtime Monitor. Proceedings of the Runtime Verification: First International Conference, RV 2010, St. Julians, MT, USA.","DOI":"10.1007\/978-3-642-16612-9"},{"key":"ref_44","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/s10703-013-0199-z","article-title":"Runtime Verification of Embedded Real-Time Systems","volume":"44","author":"Reinbacher","year":"2014","journal-title":"Form. Methods Syst. Des."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.jnca.2018.06.001","article-title":"Velox VM: A safe execution environment for resource-constrained IoT applications","volume":"118","author":"Tsiftes","year":"2018","journal-title":"J. Netw. Comput. Appl."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2811267","article-title":"Terra: Flexibility and Safety in Wireless Sensor Networks","volume":"11","author":"Branco","year":"2015","journal-title":"ACM Trans. Sen. Netw."},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2010.12.013","article-title":"Feature Interaction Aware Test Case Generation for Embedded Control Systems","volume":"264","author":"Lochau","year":"2010","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Zhang, C., Bai, X., Li, J., and Zhang, R. (2013, January 29\u201330). Automated Test Case Generation for Embedded Software Using Extended Interface Automata. Proceedings of the 2013 13th International Conference on Quality Software, Najing, China.","DOI":"10.1109\/QSIC.2013.24"},{"key":"ref_49","first-page":"860","article-title":"Test Case Generation for Embedded System Software using UML Interaction Diagram","volume":"12","author":"Mani","year":"2017","journal-title":"J. Eng. Sci. Technol."},{"key":"ref_50","doi-asserted-by":"crossref","first-page":"710","DOI":"10.1109\/TII.2018.2840534","article-title":"WSN Design and Verification Using On-Board Executable Specifications","volume":"15","author":"Gaglio","year":"2019","journal-title":"IEEE Trans. Ind. Inform."},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Rather, E.D., Colburn, D.R., and Moore, C.H. (1993). The Evolution of Forth. Proceedings of the HOPL-II Second ACM SIGPLAN Conference on History of Programming Languages, ACM.","DOI":"10.1145\/154766.155369"},{"key":"ref_52","unstructured":"Pelc, S. (2020, December 25). Programming Forth. Available online: https:\/\/www.mpeforth.com\/arena\/ProgramForth.pdf."},{"key":"ref_53","doi-asserted-by":"crossref","unstructured":"Gaglio, S., Lo Re, G., Martorella, G., and Peri, D. (2015, January 16\u201319). Programming Distributed Applications with Symbolic Reasoning on WSNs. Proceedings of the 2015 International Conference on Computing, Networking and Communications (ICNC), Anaheim, CA, USA.","DOI":"10.1109\/ICCNC.2015.7069340"},{"key":"ref_54","doi-asserted-by":"crossref","unstructured":"Gaglio, S., Lo Re, G., Martorella, G., and Peri, D. (2019, January 18\u201321). A Lightweight Network Discovery Algorithm for Resource-constrained IoT Devices. Proceedings of the 2019 International Conference on Computing, Networking and Communications (ICNC), Honolulu, HI, USA.","DOI":"10.1109\/ICCNC.2019.8685589"},{"key":"ref_55","doi-asserted-by":"crossref","unstructured":"Augello, A., D\u2019Antoni, R., Gaglio, S., Lo Re, G., Martorella, G., and Peri, D. (2020, January 8\u201311). Verification of Symbolic Distributed Protocols for Networked Embedded Devices. Proceedings of the 2020 25th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA), Vienna, Austria.","DOI":"10.1109\/ETFA46521.2020.9212134"},{"key":"ref_56","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/JPROC.2011.2160929","article-title":"Modeling Cyber-Physical Systems","volume":"100","author":"Derler","year":"2012","journal-title":"Proc. IEEE"},{"key":"ref_57","unstructured":"Trute, M. (2020, December 25). AmForth Documentation. Available online: http:\/\/amforth.sourceforge.net."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/1\/107\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T10:46:30Z","timestamp":1760179590000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/21\/1\/107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,26]]},"references-count":57,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2021,1]]}},"alternative-id":["s21010107"],"URL":"https:\/\/doi.org\/10.3390\/s21010107","relation":{},"ISSN":["1424-8220"],"issn-type":[{"type":"electronic","value":"1424-8220"}],"subject":[],"published":{"date-parts":[[2020,12,26]]}}}