Multipath verification of data transforms in a system of systems
Inventors
Dutertre, Bruno • Jha, Susmit • Sanchez, Huascar • Lincoln, Patrick • Pearson, Eric M. • Dean, Richard • Mason, Ian A.
Assignees
Publication Number
US-12321326-B2
Publication Date
2025-06-03
Expiration Date
2041-12-17
Interested in licensing this patent?
MTEC can help explore whether this patent might be available for licensing for your application.
Abstract
Processing circuitry is configured to obtain a data structure that defines a plurality of conversions of data between pairs of fields; perform a search to identify a plurality of paths from a source node of the data structure to a destination node of the data structure, wherein the source node corresponds to a first field of the fields and the destination node corresponds to a second field of the fields; convert, for each path of the plurality of paths, transforms represented by corresponding edges of the path to a sequence of transforms that conform to a solver format; process the sequence of transforms for each path to determine whether all paths of the plurality of paths are equivalent up to an equivalence relation; and output an indication of whether all paths of the plurality of paths are equivalent up to an equivalence relation.
Core Innovation
The invention provides techniques for verifying whether multiple data transformation paths within a system of systems (SoS) are equivalent using a data structure that models those systems and their interconnections. The data structure, typically a field and transform graph (FTG), defines various data format fields as nodes and the transforms that convert between those formats as directed edges. A path through this structure corresponds to a specific sequence of data transforms that can convert data from a source message format to a destination message format, possibly through intermediate nodes and transforms.
The problem addressed is the increasing complexity and reduced predictability when subsystems within an SoS exchange data using different message formats. Traditional approaches, such as enforcing common message formats or developing one-to-one translation tools, can be inefficient and do not scale well as the number of subsystems or message formats increases. These limitations lead to reduced interoperability, increased development time and costs, and difficulties in integrating or updating systems.
The core innovation is a method where processing circuitry obtains the FTG, then systematically searches for all possible paths or sequences of transforms between specified source and destination fields. For each path, the transforms are expressed as compositions in a programming language format (such as a domain-specific language), then converted to a solver-compatible format (such as that accepted by a satisfiability solver). The solver is used to check if all these paths yield equivalent results up to an equivalence relation. The system outputs whether the equivalence assertion holds, facilitating interoperability assurance, consistency, and incremental updating of the transformation paths.
Claims Coverage
The independent claims define three main inventive features focused on multipath verification of data transforms using programmable and solver-based processes in a system of systems.
Method for multipath verification using data structure, path search, and solver-based equivalence checking
A method that consists of: - Obtaining a data structure that defines conversions between pairs of fields. - Performing a search to identify multiple paths from a source node (first field) to a destination node (second field). - For each path, converting transforms represented by edges to a sequence, expressing as a composition in a programming language format, and converting to a solver format. - Using a satisfiability solver to determine whether all paths are equivalent up to an equivalence relation which is reflexive, symmetric, and transitive. - Outputting an indication of equivalence and, if all paths are equivalent, storing a single representative path for future processing when additional paths are added.
Method for verifying equivalence after updates to the data structure
A method comprising: - Obtaining an updated data structure where a new set of conversions between pairs of fields differs from a previous one. - Searching to identify first and second paths from a source node to a destination node, where the second path involves at least one new field. - Converting transforms for both paths into a sequence in solver format. - Using a satisfiability solver to determine whether the two paths are equivalent up to an equivalence relation (reflexive, symmetric, transitive). - Outputting an indication of equivalence for the paths.
System for automated multipath path equivalence verification and incremental updating
A system comprising processing circuitry configured to: - Obtain a data structure defining conversions between pairs of fields. - Identify multiple paths from a source to a destination node. - For each path, convert and express transforms in a programming language format and translate to solver format. - Use a satisfiability solver for equivalence checking up to an equivalence relation. - Output the result and, if equivalent, store a single representative path for future processing as new paths are added.
In summary, the inventive features are centered around methods and systems for verifying the equivalence of multiple data transformation paths using programmable compositions and solver-based validation, supporting incremental updates and efficient future processing.
Stated Advantages
Facilitates interoperability of existing components that may not have been originally designed to cooperate.
Reduces the time and cost of building systems of systems by enabling automated verification of data transformation path equivalence.
Improves the validity and consistency of message format conversions performed by nodes of the system.
Permits incremental checking of path equivalence, avoiding unnecessary recomputation after small updates to the data structure.
Helps identify and debug errors in data transformation definitions by providing counterexamples when equivalence fails.
Documented Applications
Verification of data format conversions among subsystems in aerospace platforms, such as multiple airplanes exchanging messages over diverse networks.
Ensuring interoperable communications among smart devices, such as smart watches, smart weighing machines, and smartphones using different message formats within the Internet of Things.
Interested in licensing this patent?