{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T07:07:26Z","timestamp":1763017646365,"version":"build-2065373602"},"reference-count":33,"publisher":"MDPI AG","issue":"2","license":[{"start":{"date-parts":[[2016,6,7]],"date-time":"2016-06-07T00:00:00Z","timestamp":1465257600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems"],"abstract":"<jats:p>Waterway and canal systems are particularly cost effective in the transport of bulk and containerized goods to support global trade. Yet, despite these benefits, they are among the most under-appreciated forms of transportation engineering systems. Looking ahead, the long-term view is not rosy. Failures, delays, incidents and accidents in aging waterway systems are doing little to attract the technical and economic assistance required for modernization and sustainability. In a step toward overcoming these challenges, this paper argues that programs for waterway and canal modernization and sustainability can benefit significantly from system thinking, supported by systems engineering techniques. We propose a multi-level multi-stage methodology for the model-based design, simulation and formal verification of automated waterway system operations. At the front-end of development, semi-formal modeling techniques are employed for the representation of project goals and scenarios, requirements and high-level models of behavior and structure. To assure the accuracy of engineering predictions and the correctness of operations, formal modeling techniques are used for the performance assessment and the formal verification of the correctness of functionality. The essential features of this methodology are highlighted in a case study examination of ship and lock-system behaviors in a two-stage lock system.<\/jats:p>","DOI":"10.3390\/systems4020023","type":"journal-article","created":{"date-parts":[[2016,6,7]],"date-time":"2016-06-07T11:17:28Z","timestamp":1465298248000},"page":"23","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model-Based Design and Formal Verification Processes for Automated Waterway System Operations"],"prefix":"10.3390","volume":"4","author":[{"given":"Leonard","family":"Petnga","sequence":"first","affiliation":[{"name":"Department of Civil and Environmental Engineering, University of Maryland, College Park, MD 20742, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Austin","sequence":"additional","affiliation":[{"name":"Department of Civil and Environmental Engineering and Institute for Systems Research, University of Maryland, College Park, MD 20742, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1968","published-online":{"date-parts":[[2016,6,7]]},"reference":[{"key":"ref_1","unstructured":"Grier, D.V. (2005). The Declining Reliability of the U.S. InlandWaterway System."},{"key":"ref_2","unstructured":"Jackson, D.E. (2007). Leveraging the Strategic Value of the U.S. Inland Waterway System, USAWC Strategy Research Project, US Army War College, Carlisle Barracks."},{"key":"ref_3","unstructured":"Iowa Department of Transportation (2013). U.S. Inland Waterway Modernization: A Reconnaissance Study."},{"key":"ref_4","unstructured":"Schexnayder, C.J. (2007). Firms Eye Billions in Expansion Work At Panama Canal. ENR Eng. News-Rec., Available online: http:\/\/panama-guide.com\/."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1049\/cce:20060403","article-title":"All Locked Up","volume":"17","author":"James","year":"2006","journal-title":"Comput. Control Eng."},{"key":"ref_6","first-page":"88","article-title":"Formal Development and Evaluation of Narrow Passageway System Operations","volume":"34","author":"Kaisar","year":"2006","journal-title":"Eur. Transp."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1061\/(ASCE)0887-3801(2007)21:5(373)","article-title":"Synthesis and Validation of High-Level Behavior Models for Narrow Waterway Management Systems","volume":"21","author":"Kaisar","year":"2007","journal-title":"J. Comput. Civ. Eng. ASCE"},{"key":"ref_8","unstructured":"UPPAAL: An integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata. Available online: http:\/\/www.uppaal.com\/."},{"key":"ref_9","unstructured":"SysML Plugin, No Magic Inc.. Available online: http:\/\/www.nomagic.com\/products\/magicdraw-addons\/sysml-plugin.html."},{"key":"ref_10","unstructured":"Fritzson, P. (2003). Principles of Object-Oriented Modeling and Simulation with Modelical 2.1, John Wiley and Sons."},{"key":"ref_11","first-page":"48","article-title":"Passage to 2000: Modernization of the Panama Canal","volume":"69","author":"Gribar","year":"1999","journal-title":"Civ. Eng. Mag."},{"key":"ref_12","unstructured":"Moore, M. The Bosporus: A Clogged Artery. The Washington Post. Available online: http:\/\/www.washingtonpost.com\/."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Wieringa, R. (2003). Design Methods for Reactive Systems: Yourdon, Statemate, and the UML, Morgan Kaufmann Publishers.","DOI":"10.1016\/B978-155860755-2\/50004-6"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0191-2615(97)00003-9","article-title":"Metamodels for Estimating Waterway Delays Through a Series of Queues","volume":"32","author":"Dai","year":"1998","journal-title":"Transport. Res."},{"key":"ref_15","first-page":"232","article-title":"An Analysis of Towboat Delays","volume":"2","author":"DeSalvo","year":"1968","journal-title":"J. Transp. Econ. Policy"},{"key":"ref_16","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1061\/(ASCE)0733-950X(1998)124:4(199)","article-title":"Integrated Control For Series of Waterway Locks","volume":"124","author":"Ting","year":"1998","journal-title":"ASCE J. Waterw. Port Coast. Ocean Eng."},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1017\/S0890060499135017","article-title":"Queuing Network Analysis for Waterways with Artificial Neural Networks","volume":"13","author":"Zhu","year":"1998","journal-title":"Artif. Intell. Eng. Des. Anal. Manuf."},{"key":"ref_18","unstructured":"Austin, M.A., Baras, J.S., and Kositsyna, N.I. (August, January 28). Combined Research and Curriculum Development in Information-Centric Systems Engineering. Proceedings of the Twelth Annual International Symposium of the International Council on Systems Engineering (INCOSE), Las Vegas, NV, USA."},{"key":"ref_19","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1002\/sys.20049","article-title":"PaladinRM: Graph-Based Visualization of Requirements Organized for Team-Based Design","volume":"9","author":"Austin","year":"2006","journal-title":"Syst. Eng."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1038\/scientificamerican0606-68","article-title":"Dependable Software by Design","volume":"294","author":"Jackson","year":"2006","journal-title":"Sci. Am."},{"key":"ref_21","first-page":"1","article-title":"Platforms for Engineering Experimental Biomedical Systems","volume":"9","author":"Mosteller","year":"2014","journal-title":"IEEE Syst. J."},{"key":"ref_22","unstructured":"Fridenthal, S., Moore, A., and Steiner, R. (2008). A Practical Guide to SysML, The MK-OMG Press."},{"key":"ref_23","unstructured":"Unified Modeling Language (UML). Available online: http:\/\/www.omg.org\/uml."},{"key":"ref_24","unstructured":"Wellstead, P.E. (2000). Introduction to Physical System Modelling. Control Systems Principles, Academic Press Ltd."},{"key":"ref_25","unstructured":"Hooman, J. (2001). Introduction to Timed Systems, University of Nijmegen."},{"key":"ref_26","unstructured":"Slind, K. (2004). Class Notes on Theory of Computation, Department of Computer Science, University of Utah."},{"key":"ref_27","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_28","unstructured":"Graves, H. (2012, January 9\u201312). Integrating Reasoning with SysML. Proceedings of the INCOSE International Symposium, Rome, Italy."},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Eppinger, S.D., and Browning, T.D. (2012). Design Structure Matrix Methods and Applications, The MIT Press.","DOI":"10.7551\/mitpress\/8896.001.0001"},{"key":"ref_30","unstructured":"MagicDraw. Available online: http:\/\/www.nomagic.com\/products\/magicdraw.html."},{"key":"ref_31","unstructured":"The Jython Project. Available online: http:\/\/www.jython.org."},{"key":"ref_32","unstructured":"Functional Mock-up Interface Standard for Model Exchange and Tool Coupling. Available online: https:\/\/www.fmi-standard.org."},{"key":"ref_33","unstructured":"Brauer, J., and Moller, O. Techniques for Abstraction of Continuous-Time Models into Finite Discrete-Event Models for Model Checking. Technical Note D5.1c, Version: 0.3, Horizon 2020: Integrated Tool Chain for Model-Based Design of CPSs. Available online: http:\/\/into-cps.au.dk."}],"container-title":["Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2079-8954\/4\/2\/23\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T19:25:08Z","timestamp":1760210708000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2079-8954\/4\/2\/23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,7]]},"references-count":33,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2016,6]]}},"alternative-id":["systems4020023"],"URL":"https:\/\/doi.org\/10.3390\/systems4020023","relation":{},"ISSN":["2079-8954"],"issn-type":[{"type":"electronic","value":"2079-8954"}],"subject":[],"published":{"date-parts":[[2016,6,7]]}}}