A. James Clark School of Engineering

Permanent URI for this communityhttp://hdl.handle.net/1903/1654

The collections in this community comprise faculty research works, as well as graduate theses and dissertations.

Browse

Search Results

Now showing 1 - 3 of 3
  • 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.
  • Thumbnail Image
    Item
    Semantic-driven modeling and reasoning for enhanced safety of cyber-physical systems
    (2016) Petnga, Leonard; Austin, Mark; Civil Engineering; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)
    This dissertation is concerned with the development of new methodologies and semantics for model-based systems engineering (MBSE) procedures for the behavior modeling of cyber-physical systems (CPS). Our main interest is to enhance system-level safety through effective reasoning capabilities embedded in procedures for CPS design. This class of systems is defined by a tight integration of software and physical processes, the need to satisfy stringent constraints on performance, safety and a reliance on automation for the management of system functionality. Our approach employs semantic–driven modeling and reasoning : (1) for the design of cyber that can understand the physical world and reason with physical quantities, time and space, (2) to improve synthesis of component-based CPS architectures, and (3) to prevent under-specification of system requirements (the main cause of safety failures in software). We investigate and understand metadomains, especially temporal and spatial theories, and the role ontologies play in deriving formal, precise models of CPS. Description logic-based semantics and metadomain ontologies for reasoning in CPS and an integrated approach to unify the semantic foundations for decision making in CPS are covered. The research agenda is driven by Civil Systems design and operation applications, especially the dilemma zone problem. Semantic models of time and space supported respectively by Allen’s Temporal Interval Calculus (ATIC) and Region Connectedness Calculus (RCC-8) are developed and demonstrated thanks to the capabilities of Semantic Web technologies. A modular, flexible, and reusable reasoning-enabled semantic-based platform for safety-critical CPS modeling and analysis is developed and demonstrated. The platform employs formal representations of domains (cyber, physical) and metadomains (temporal and spatial) entities using decidable web ontology language (OWL) formalisms. Decidable fragments of temporal and spatial calculus are found to play a central role in the development of spatio-temporal algorithms to assure system safety. They rely on formalized safety metrics developed in the context of cyber-physical transportation systems and collision avoidance for autonomous systems. The platform components are integrated together with Whistle, a small scripting language (under development) able to process complex datatypes including physical quantities and units. The language also enables the simulation, visualization and analysis of safety tubes for collision prediction and prevention at signalized and non-signalized traffic intersections.