Civil & Environmental Engineering Research Works

Permanent URI for this collectionhttp://hdl.handle.net/1903/1657

Browse

Subject: search.filters.subject.automation

Search Results

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Model-Based Design and Formal Verification Processes for Automated Waterway System Operations
    (MDPI, 2016-06-07) Petnga, Leonard; Austin, Mark
    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.
  • Thumbnail Image
    Item
    Compositional Approach to Distributed System Behavior Modeling and Formal Validation of Infrastructure Operations with Finite State Automata: Application to Viewpoint-Driven Verification of Functionality in Waterways
    (MDPI, 2018-01-12) Austin, Mark A.; Johnson, John
    Now that modern infrastructure systems are moving toward an increased use of automation in their day-to-day operations, there is an emerging need for new approaches to the formal analysis and validation of system functionality with respect to correctness of operations. This paper describes a compositional approach to the multi-level behavior modeling and formal validation of large-scale distributed system operations with hierarchies and networks of finite state automata. To avoid the well-known state explosion problem, we develop a new procedure for viewpoint-action-process traceability, thereby allowing parts of a behavior model not relevant to a specific decision to be removed from consideration. Key features of the methodology are illustrated through the development of behavior models and validation procedures for polite conversation between two individuals, and lockset- and system-level concerns for ships traversing a large-scale waterway system.