United States

SysML (Systems Modeling Language) is a widely-used formalism and international standard for designing and communicating complex system designs, and is especially relied upon in the development of safety-critical autonomous systems. SysML v2 is a major new version of SysML currently undergoing finalization, scheduled to be released mid-2024. Among many key enhancements, SysML v2 introduces a formal semantics for specifying the precise meaning of SysML models, which makes it possible to apply formal verification and automated reasoning to analyze safety and correctness properties of SysML designs automatically.

At Imandra, we are applying our Imandra Automated Reasoning System to the design and analysis of SysML v2 models. Key to this work is a formal semantics for SysML v2 models expressed in Imandra&#39;s logic, and corresponding verification automation for answering deep questions about the possible behaviors of SysML models. In addition to verification, we can then leverage Imandra&#39;s &quot;proof-carrying prose&quot; integration with LLMs to obtain conversational assistants (chatbots) which can rigorously answer complex questions about SysML v2 designs, backing every answer up with an independently verifiable logical audit trail produced by Imandra reasoning about the SysML v2 model.

During this talk, we will demonstrate how to use Automated Reasoning with SysML v2 models to:
- Mathematically prove properties of system correctness.
- Add a hallucination-free natural-language interface (chatbot) to empower more stakeholders to gain insights and leverage the SysML v2 model.

NAML 2024

Imandra + SysML: Automated Reasoning for SysML (Systems Modeling Language) v2

sysml

mbse

automated reasoning

formal methods

The purpose of the International Conference on Model-Driven Engineering and Software Development is to provide a platform for researchers, engineers, academics as well as industrial professionals from all over the world to present their research results and development activities in using models and model driven engineering techniques for Software Development. Model-Driven Development (MDD) is an approach to the development of IT systems in which models take a central role, not only for analysis of these systems but also for their construction. MDD has emerged from modelling initiatives, most prominently the Model-Driven Architecture (MDA) fostered by the Object Management Group (OMG). In the scope of MDA, a couple of technologies have been developed that became the cornerstones of MDD, like metamodelling and model transformations. MDD relies on languages for defining metamodels, like the Meta-Object Facility (MOF) and Ecore (developed in the scope of the Eclipse Modelling Framework), and transformation specification languages like QVT and ATL. 
CONFERENCE AREAS 
1 . Methodologies, Processes and Platforms 
2 . Applications and Software Development 
3 . Modeling Languages, Tools and Architectures

MODELSWARD 2022

The purpose of the International Conference on Model-Driven Engineering and Software Development is to provide a platform for researchers, engineers, academics as well as industrial professionals from all over the world to present their research results and development activities in using models and model driven engineering techniques for Software Development. 

SysML (Systems Modeling Language) is a widely-used formalism and international standard for designing and communicating complex system designs, and is especially relied upon in the development of safety-critical autonomous systems. SysML v2 is a major new version of SysML currently undergoing finalization, scheduled to be released mid-2024. Among many key enhancements, SysML v2 introduces a formal semantics for specifying the precise meaning of SysML models, which makes it possible to apply formal verification and automated reasoning to analyze safety and correctness properties of SysML designs automatically.

At Imandra, we are applying our Imandra Automated Reasoning System to the design and analysis of SysML v2 models. Key to this work is a formal semantics for SysML v2 models expressed in Imandra's logic, and corresponding verification automation for answering deep questions about the possible behaviors of SysML models. In addition to verification, we can then leverage Imandra's "proof-carrying prose" integration with LLMs to obtain conversational assistants (chatbots) which can rigorously answer complex questions about SysML v2 designs, backing every answer up with an independently verifiable logical audit trail produced by Imandra reasoning about the SysML v2 model.

During this talk, we will demonstrate how to use Automated Reasoning with SysML v2 models to:
- Mathematically prove properties of system correctness.
- Add a hallucination-free natural-language interface (chatbot) to empower more stakeholders to gain insights and leverage the SysML v2 model.

poster

### Welcome to the 8th annual workshop on Naval Applications of Machine Learning!

NAML is the premier annual event showcasing current machine learning research relevant to Naval applications. We welcome participation from the defense community, industry, and academia. The NAML workshop is an opportunity for researchers from Navy research and development centers and our partner organizations to exchange technical ideas and to come together as a team.

The goals of NAML are:

* To spread awareness of current machine learning research relevant to Naval applications

* To connect machine learning researchers with experts in military requirements

* To build and strengthen collaborations within the defense research community

Naval Information Warfare Center Pacific is partnering with AFCEA San Diego chapter to host the workshop.

**General Chairs:**

Katie Rainey, Naval Information Warfare Center Pacific

Nicole Isoda, Naval Information Warfare Center Pacific 

**[More about NAML 2024](https://sites.google.com/go.spawar.navy.mil/naml/)**

Please log in to explore this event. You need to log in with the email address you registered with. Access credentials have been sent to your email. 

Please be sure to check your spam and other email folders if you do not see an email confirmation right away.

Please log in to explore this workshop.

Registration for this workshop has now closed. We appreciate your interest and hope to welcome you at a future event. If you’d like to hear about similar upcoming events, please check our website or join our mailing list.

Registration for this workshop has now closed.

The 8th annual workshop on Naval Applications of Machine Learning is an opportunity for researchers from Navy research and development centers and our partner organizations to exchange technical ideas and to come together as a team. The goals of NAML are to spread awareness of current machine learning research relevant to Naval applications, to connect machine learning researchers with experts in military requirements and to build and strengthen collaborations within the defense research community.


The ever-growing size of deep learning models necessitates more extensive resources, making them unsuitable for tasks requiring lower latency and less computational power. This is particularly true for edge devices. Multiple compression techniques have been developed to bring the capabilities of these larger models to a smaller form factor, one of the most successful of which has been knowledge distillation. Knowledge distillation is employed to transfer knowledge from a large "teacher" model to a smaller "student" model. This technique facilitates learning a compressed representation of data, maintaining the performance benefits of large models while reducing computational and memory demands. It involves training the student model on both hard labels and soft labels provided by the teacher model, leading to better generalization and informed predictions.

Our work increases the effectiveness of knowledge distillation by augmenting the labels of both the teacher and student models with a vector quantized vector. Vector quantization is a mapping of high-dimensional data to a lower-dimensional codebook, effectively reducing data dimensionality. This technique has traditionally been applied to speech and image compression particularly in Variational Autoencoders (VQ-VAEs), and has proven effective at markedly increasing the effectiveness of student models to learn from teacher model representations.

The work presented here seeks to enhance the classification capabilities of the student model, carefully maintaining its compact size to balance efficiency and compactness. This approach improves retained knowledge distillation performance, while conferring model interpretability benefits. We show that while also increasing student model classification performance, the inclusion of the VQ layer also provides a measure for detecting classification quality and detect data which is out of distribution. This approach promises to increase the capabilities of edge deployed models both with respect to their mission performance as well as out of distribution detection.


Improving Knowledge Distillation with Discrete Feature Vector Representation

My poster presentation explains documented co-symbolic AI decision support and automated security. It includes contracted use and exercise support with US Special Operations Command; US Army Intelligence Command; US Army Program Executive Officer for Simulation, Training, and Instrumentation; and the US Marine Corps Tactical Operation Group. By Light combines a mature multi-domain warfighting knowledge graph symbolic AI (expert system), a budding self-supervising artificial general intelligence (AGI), and a proven faster than real-time wargaming tool. Each of the parts come together to support warfighting decisions while overcoming critical warfighting AI vulnerabilities, not achievable by most AI. These include 1) allowing risk manageability/trust across assurance, attribution, understanding, traceability, and bias; 2) preventing model collapse; 3) eliminating human data annotation bias and expense; 4) affording real-time data tag, label, aggregation, and neural networking with minimal if any latency regardless of schema, structure, or unstructured; 5) surmounting data latency - neural networking 10 petabytes of historical data in less than year; 6) acting as master middleware, applying all data and integrating all apps with low cost of entry - only web capable; 7) learning warfighter user behavior, optimizing and customizing to predominantly push answers instead of users always querying an answer; 8) learning operating environment behavior in real-time and recognizing asymmetry; 9) applying multi-domain warfighter expertise across all battle and warfighting functions; and 10) cyber-securing artificial intelligence automation across all information technology, operational technology, and internet of things infrastructure, because it takes AI to secure AI.
The presentation will include government results from theater and tactical level multi-domain peer-to-peer exercises and video demonstration of the parts. It will challenge the audience to consider the warfighting vulnerabilities present in other AI, such as ChatGPT and introduce a suitable, feasible, secure, trustworthy, and acceptable path for warfighter AI decision support.


Knowledge Enhanced Multi-domain Artificial Intelligence

Naval Asset Corrosion and Defect Segmentation Using UNet Architecture 

Abstract: 

Corrosion poses a significant challenge in the maintenance and upkeep of naval assets, leading to degradation and high cost. Timely and accurate detection of corrosion and other defects are crucial to ensure operational efficiency and system availability. Traditional methods for detection often involve manual inspections, which are time-consuming, prone to human error, and require inspectors with specialized training and expertise. 

There is a significant amount of research into automatic detection of corrosion via computer vision algorithms and semantic segmentation that we utilized to combat this problem. Our method makes use of hand-annotated high-resolution images of existing weathered structures (conex boxes) as inputs for a machine learning model to detect basic corrosion, as well as classify additional defects such as paint blistering and cracking. Due to the limited amount of data representing the extended classes, image augmentations were performed to expand our dataset. 

When classifying “stuff”, where the defects can be any shape or size, having an extremely high level of precision is necessary. To account for this, a UNet machine learning architecture, which consists of a contracting and symmetric expanding path, was chosen due to its capability of performing precise pixel-level image segmentation with fewer training data requirements. We have experimented with multiple variations of UNet and implemented additional modules like attention and deep supervision in order to increase the overall performance and generalization of the model.

Naval Asset Corrosion and Defect Segmentation Using UNet Architecture 

Overhead imaging sensors can positively contribute to Maritime Domain Awareness (MDA) missions. The Naval Center for Space Technology at the Naval Research Laboratory (NRL) continuously investigates the latest technologies for space-based sensing. This poster presentation provides an overview of ongoing Artificial Intelligence (AI) and Machine Learning (ML) projects being conducted by the center. Project topics include Automatic Target Recognition (ATR), automated detection of sensor anomalies, scene simulation, and the associated components (e.g. optics, sensors, processing electronics) that enable these projects. NRL has examined the performance of different AI-based vessel detection models on space-ready electronics. NRL has evaluated AI-based methods to detect sensor anomalies. NRL has stood up a laboratory to develop, test, and validate algorithms using simulated overhead scenes. This poster presentation will provide information on each of these efforts.

Overview of AI/ML projects at Naval Center for Space Technology

The landscape of maritime security is rapidly evolving,
necessitating advanced surveillance and threat detection systems.
We introduce a multimodal framework employing a zero-shot
approach designed for detecting anomalies, novelty, and out-
of-distribution (OOD) events, particularly focusing on warships
and fishing vessels. This system, utilizing a pretrained model for
feature extraction, innovatively integrates high-resolution
satellite imagery, drone videos, and radio frequency data. The
fusion of these diverse data modalities into a unified latent feature
space significantly enhances precision, recall, and accuracy in
anomaly detection, while substantially reducing the noise
associated with individual modalities. This improvement stems
from the richer contextual information provided by the multimodal
fusion.
The framework features a user-centric design, allowing
operators to specify regions of interest (ROI) for monitoring
through an intuitive interface. This approach ensures that
vigilance is focused on critical areas, thus improving the relevance
and precision of threat detection. Within these ROIs, our zero-
shot transformer-based multimodal clustering algorithm
analyzes naval movement patterns, comparing them against
established normative behaviors derived from historical data.
This method efficiently filters anomalies, uncovers novel
behaviors, and enhances OOD detection by flagging significant
deviations from the training labels distribution.
Upon detecting a behavioral change within an ROI, the system
promptly issues alerts to operators. These alerts are enriched
with contextual information from the multimodal data
sources, including visual confirmations from drone footage and
satellite imagery, ensuring operators receive a comprehensive
understanding of the situation for swift and informed decision-
making.
Our proposed framework represents a significant advancement in
maritime security, setting a precedent for adaptable and scalable
surveillance systems across various domains. Its ability to
integrate new data types and sources, combined with its focus on
user-defined areas of interest, renders it a robust and versatile
tool for current and future security challenges. Empowering
operators to monitor specific maritime regions effectively and
leveraging advanced multimodal machine learning techniques for
threat detection, the proposed approach is set to revolutionize
naval surveillance and security.

Precision Maritime Monitoring: Integrated Anomaly, Novelty, and OOD Detection in Designated Naval Areas

Active learning seeks to minimize annotation costs by selecting the most useful training data for deep machine learning models. However, until recently, the most successful active learning algorithms have required a large initial labeled set to work properly. This makes them impractical for labor-intensive labeling tasks such as object detection and modalities such as synthetic aperture radar (SAR). Improvements in extracting useful intrinsic features from unlabeled data through self-supervised learning have reduced the need for large amounts of labeled data. As a result, AL can focus on selecting a smaller subset of the best data to label for supervised learning on downstream tasks. Since annotation costs tend to be higher for these downstream tasks, it is crucial that the AL algorithm perform well under low annotation budgets. In this work, we study feature representations for AL in the low-budget regime specifically. Our AL approach builds upon existing self-supervised representation learning methods by leveraging features learned from pretrained models and applying them to the SAR modality. Using these self-supervised learned features, we employ a diversity-based sampling strategy to select the examples for labeling under a low annotation budget. Qualitative results indicate that self-supervision with datasets well-matched to the target domain, when combined with cluster sampling-based AL algorithms, can lead to the selection of diverse samples.

Representations for Low-Budget Synthetic Aperture Radar (SAR) Active Learning

Many of the current state of the art Intelligent Autonomous Systems (IAS) and robotics systems use Inertial Measurement Units (IMU) for navigation and control. This includes, Boston Dynamics SPOT, Ghost Robotics quadrupeds, Clearpath Warthog, and numerous UAS systems all of which are being tested for military applications. IMU sensor allows for a high-resolution measurements of the orientation, angular velocity, linear velocity of the IAS. These measurements assume a stationary frame reference; this assumption does not hold in a moving reference frame such as an aircraft carrier which is has six degrees of freedom. The moving reference frame of the aircraft carrier will cause measurement errors for IAS systems which can cause their controller and navigation systems to fail. The magnitude of the effect is unknown leaving a large gap in knowledge.

SEA LEGS: Ship Experiments for Autonomous Locomotion and Guidance Euler Systems

The goal of this work is to create a robotic subsystem that is capable of effectively fighting fires in a shipboard environment both autonomously and via teleoperation. The system will be designed as a firefighting attachment for mobile robots incorporated into the fleet in the future. SAFERS will use a COTS motorized firefighting monitor, a variable power aimed water cannon, to target and extinguish fires. The targeting control software will allow for both automatic targeting of the fire and manual targeting control by an operator. Both automatic and manual targeting decisions will be informed by the various cameras that make up the perception system. The perception system will also use the video feeds to identify fires and hotspots within the fires to provide ideal targeting suggestions to most effectively fight fires. A variety of different perception sensors will be explored in order to test their effectiveness for firefighting tasks in a complex environment. Additionally, various learning and classical vision algorithms will be trained and tested to evaluate performance in the tasks of fire and hot spot detection across sensor spectrums. Some of the machine learning methods currently being explored are deep convolutional neural networks and visual transformers for object detection, semantic segmentation, and monocular depth estimation. The detected objects and estimated depths of the environments will be used by the control algorithms to make intelligent targeting decisions during firefighting scenarios. Ideally, the developed system will be useful tool for fleet firefighters as both an autonomous and remote system that will lower risk to sailors while simultaneously improving overall firefighting capability.



Semi-Autonomous Fire Extinguishing Robot Subsystem (SAFERS)

In the present scenario, Unmanned Surface Vehicles (USVs) or Uncrewed Surface Vessels are playing vital role in naval combat. Many researchers across the globe are working on various applications environmental monitoring and enemy prediction location. While undertaking naval combat missions especially in extreme weather conditions, a real time environment plays a vital role to achieve autonomous navigation and completing tasks for USVs. This is performed for accuracy in detection and recognition of any object that is likely to be an obstacle causing a potential danger to the sailing ships on the water surface. There is a limit in the availability of datasets for many scenarios from publicly available datasets. The data can be collected manually, and this procedure takes several days. This process is expensive and time consuming. Once ample datasets are available, it is easy to train the machine learning model. To address the issue, this research work proposes on implementing synthetic image data from the real images. The image data that is generated, optimizes the data collection process and produces a significant amount of data that could help training ML models with the help of Generative Adversarial Networks (GANs). The implementation of this proposed technique is achieving better accuracy. This research work also finds the generator and discriminator losses and scores of real and synthetic data of the GAN. 


Synthetic data for Naval Combats using Generative Adversarial Networks

In this work, we expanded on the Constrained Few-Shot Class Incremental Learning (C-FSCIL) framework, which breaks up the monolithic structure of a DNN into 1) a frozen pre-trained feature extractor, 2) a retrainable fully connected layer, and 3) an explicit prototype vector memory matrix. We investigate how the feature extractor architecture, learning strategy, and output dimension affect C-FSCIL performance. Our implementation of the C-FSCIL framework learned an additional 40 classes over the 60 in the base session, with a final accuracy of 78.4%, a 28%-point improvement over the ResNet12 baseline.

Premium content

Next from NAML 2024

Improving Knowledge Distillation with Discrete Feature Vector Representation

Similar lecture

Rigorous Modelling of Quantities for Model-Based Systems Engineering