Browsing by Author "Johnson, John"

Now showing 1 - 3 of 3
  • 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
    Compositional Behavior Modeling and Formal Validation of Canal System Operations with Finite State Automata
    (2011-06) Austin, Mark; Johnson, John
    Traditional approaches to the formal analysis of canal system operations focus on performance. However, now that canal system operations are moving toward increased use of automation in their day-to-day operations, there is a strong need for formal analysis of system functionality with respect to correctness of operations. This report describes a compositional approach to the multi-level behavior modeling and formal validation of canal system operations with hierarchies and networks of finite state automata. Models and specifications of behavior are formally designed as labeled transition systems. To avoid the well-known state explosion problem, we develop a new procedure for viewpoint-action-process traceability, thereby allowing parts of a problem not relevant to a specific decision to be removed from consideration. Key features of the methodology are illustrated through development of behavior models and validation procedures for lockset- and system-level concerns in the Panama Canal System.
  • Thumbnail Image
    Item
    LTSA Modeling of the Panama Canal
    (2007-08-21) Johnson, John
    To research, discover, and apply methods of system analysis and control for modeling the Panama Canal using the Labeled Transition System Analyzer Tool.