A Formal Engineering Approach to High-Level Design of Situation Analysis Decision Support Systems

We apply the Abstract State Machine (ASM) method and the CoreASM tool to design and analysis of Situation Analysis Decision Support (SADS) systems. Realistic situation analysis scenarios routinely deal with situations involving multiple mobile agents reacting to discrete events distributed in space and time. SADS system engineering practices call for systematic formal modeling approaches to manage complexity through modularization, refinement and validation of abstract models. We explore here SADS system design based on ASM modeling techniques paired with CoreASM tool support to facilitate analysis of the problem space and reasoning about design decisions and conformance criteria so as to ensure they are properly established and well understood prior to building the system. We provide an extension to CoreASM for the Marine Safety & Security domain, specifically for capturing rendezvous scenarios. The extension yields the necessary background concepts, such as mobile sensors and shipping lanes, and offers runtime visualization of simulation runs together with an analyzer to measure success of various rendezvous detection strategies used in the model. We illustrate the application of the proposed approach using a sample rendezvous scenario.