Description:FIELD OF THE INVENTION
[0001] The present invention relates to the field of runtime verification and formal methods for embedded systems, and more particularly to a hardware-accelerated system and method for abstraction-based runtime property verification of safety-critical embedded controllers using field programmable gate arrays and application-specific integrated circuits.

DESCRIPTION OF THE RELATED ART
[0002] The following description of the related art is intended to provide background information pertaining to the field of disclosure. This section may include certain aspects of the art that may be related to various features of the present disclosure. However, it should be appreciated that this section is used only to enhance the understanding of the reader with respect to the present disclosure, and not as admissions of the prior art.
[0003] Runtime verification of safety-critical embedded systems has become increasingly vital as these systems are deployed in automotive braking, industrial robotics, and aircraft flight control applications where failures can result in catastrophic consequences. Traditional software-based verification approaches suffer from excessive latency and computational overhead, making them unsuitable for real-time systems operating at frequencies up to one kilohertz where verification must complete within millisecond timeframes.
[0004] Existing runtime verification techniques typically monitor concrete execution states, resulting in state space explosion as system complexity increases. These conventional approaches generate millions of states even for moderate-length executions, requiring gigabytes of memory and causing verification times to exceed practical limits. Furthermore, software-only solutions cannot meet the stringent timing constraints of embedded controllers, particularly when verifying complex temporal properties involving multiple control variables and safety conditions.
[0005] Recent advances in formal methods have introduced abstraction techniques at design-time to reduce verification complexity. However, current implementations face challenges including inability to adapt abstractions dynamically during runtime, lack of hardware acceleration for time-critical operations, and failure to preserve property correctness when transitioning from concrete to abstract models. Additionally, existing solutions cannot efficiently handle both data-oriented properties involving sensor values and control-oriented properties tracking execution flow through system modules.
[0006] Therefore, there exists a requirement for an improved abstraction-based runtime property verification system that employs hardware instrumentation interfaces using field programmable gate arrays for low-latency event capture, implements dedicated verification processors on application-specific integrated circuits for parallel property evaluation, incorporates hardware-optimized abstraction circuits for real-time state space reduction, and achieves sub-millisecond verification latency while reducing memory requirements by at least two orders of magnitude compared to concrete state monitoring approaches.

OBJECTS OF THE PRESENT DISCLOSURE
[0007] Some of the objects of the present disclosure, which at least one embodiment herein satisfies are as listed herein below.
[0008] An object of the present disclosure is to provide a system for abstraction-based runtime property verification which employs execution trace capture from a target embedded controller and constructs abstract state models through systematic reduction techniques.
[0009] An object of the present disclosure is to provide a system for abstraction-based runtime property verification which utilizes abstraction functions that partition concrete value ranges into verification zones, thereby reducing memory consumption by a factor of at least one hundred compared to storing concrete values.
[0010] An object of the present disclosure is to provide a system for abstraction-based runtime property verification which achieves real-time verification with latency below one millisecond for control systems operating at frequencies up to one kilohertz, enabling deployment in safety-critical automotive braking systems, industrial robot controllers, and aircraft flight control systems.

SUMMARY
[0011] This section is provided to introduce certain objects and aspects of the present disclosure in a simplified form that are further described below in the detailed description. This summary is not intended to identify the key features or the scope of the claimed subject matter.
[0012] The present disclosure generally relates to runtime verification systems and formal methods for embedded control systems. More particularly, the present disclosure relates to an abstraction-based runtime property verification system that employs hardware instrumentation interfaces using field programmable gate arrays for real-time event capture, dedicated verification processors on application-specific integrated circuits for parallel property evaluation, and hardware-optimized abstraction circuits for state space reduction, providing enhanced safety verification capabilities through property-preserving abstractions and sub-millisecond latency operation for safety-critical embedded controllers in automotive, industrial, and aerospace applications.
[0013] An aspect of the present disclosure relates to a system (100) for abstraction-based runtime property verification. The system comprises an execution trace (101) containing runtime events captured from a target embedded controller; a set of key attributes (102) representing monitored variables (x₁, ..., xₙ); a linear state model construction process (103) that generates a linear state model (LSM) (104) capturing all state changes for the key attributes; a distinct state model construction process (105) that eliminates duplicate states to create a distinct state model (DSM) (106); abstraction functions (107) including Boolean abstraction (111), Multi-valued abstraction (112), and Path abstraction (113) that map concrete values to abstract domains; an abstract model construction process (108) that applies the abstraction functions to generate an abstract state model (ASM) (109) with reduced state space; and a property verification process (110) that evaluates safety properties on the abstract model. The system achieves real-time verification with latency below one millisecond for control systems operating at frequencies up to one kilohertz, and the abstraction-based approach reduces verification requirements by at least two orders of magnitude compared to concrete state monitoring
[0014] In another aspect, the present disclosure relates to a method (700) for abstraction-based runtime property verification. The method comprises: intercepting (702) memory write operations and system events to generate an execution trace (101) containing event data packets with variable updates and timestamps; executing (704) model construction processes, wherein executing comprises: identifying key attributes (102) from the execution trace for monitoring; constructing a linear state model (LSM) (104) through linear state model construction (103) that captures all state changes; creating a distinct state model (DSM) (106) through distinct state model construction (105) by eliminating duplicate states; applying abstraction functions (107) including Boolean (111), Multi-valued (112), and Path (113) abstractions to partition concrete value ranges into abstract domains; generating an abstract state model (ASM) (109) through abstract model construction (108) by encoding concrete values into abstract representations, thereby reducing memory consumption by a factor of at least one hundred; and establishing state transition relationships in the abstract model; transforming (706) safety property specifications into verifiable conditions suitable for evaluation on the abstract model; executing (708) property verification (110) on the abstract state model to evaluate safety properties and detect violations in real-time
[0015] Various objects, features, aspects and advantages of the inventive subject matter will become more apparent from the following detailed description of preferred embodiments, along with the accompanying drawing figures in which like numerals represent like components.

BRIEF DESCRIPTION OF DRAWINGS
[0016] The accompanying drawings are included to provide a further understanding of the present disclosure and are incorporated in and constitute a part of this specification. The drawings illustrate exemplary embodiments of the present disclosure and, together with the description, serve to explain the principles of the present disclosure. The diagrams are for illustration only, which thus is not a limitation of the present disclosure.
[0017] FIG. 1 illustrates an exemplary representation of a block diagram of a system for abstraction-based runtime property verification, in accordance with an embodiment of the present disclosure.
[0018] FIG. 2 illustrates an exemplary schematic representation of the hardware instrumentation interface architecture depicting field programmable gate array intercepting memory write operations and generating event data packets, in accordance with an embodiment of the present disclosure.
[0019] FIG. 3 illustrates an exemplary representation of the property verification process on abstract state models, showing the decision flow between state-based checking and path-based checking with different abstraction types including Boolean, multi-valued, and path abstractions, in accordance with an embodiment of the present disclosure.
[0020] FIG. 4 illustrates an exemplary representation of the abstraction types for runtime verification, in accordance with an embodiment of the present disclosure.
[0021] FIG. 5 illustrates an exemplary representation of the abstract state model construction process, in accordance with an embodiment of the present disclosure.
[0022] FIG. 6 illustrates an exemplary block diagram depicting the integration of hardware instrumentation interface, application-specific integrated circuit, and cache memory components, in accordance with an embodiment of the present disclosure.
[0023] FIG. 7 illustrates an exemplary flow diagram depicting a method for abstraction-based runtime property verification, in accordance with an embodiment of the present disclosure.

DETAILED DESCRIPTION
[0024] The ensuing description provides exemplary embodiments only, and is not intended to limit the scope, applicability, or configuration of the disclosure. Rather, the ensuing description of the exemplary embodiments will provide those skilled in the art with an enabling description for implementing an exemplary embodiment. It should be understood that various changes may be made in the function and arrangement of elements without departing from the spirit and scope of the invention as set forth.
[0025] An aspect of the present disclosure relates to a system for abstraction-based runtime property verification including at least one hardware instrumentation interface intercepting memory operations at hardware level. The system includes at least one dedicated verification processor executing abstract model construction engines on application-specific integrated circuits. The system includes hardware-optimized abstraction circuits partitioning concrete values into safety zones. The system includes property transformation circuits converting specifications into hardware-verifiable conditions. The system includes parallel verification engines evaluating multiple states simultaneously. The system includes cache memory storing abstract state vectors and transition graphs. The system includes interrupt generation units triggering safety procedures upon violation detection. The system includes direct memory access channels enabling high-speed event packet transmission. The system achieves sub-millisecond verification latency for kilohertz-frequency control systems.
[0026] Various embodiments of the present disclosure are described using FIGs. 1 to 7.
[0027] FIG. 1 illustrates an exemplary representation of a block diagram of a system for abstraction-based runtime property verification, in accordance with an embodiment of the present disclosure.
[0028] In an embodiment, referring to FIG. 1, the system (100) for abstraction-based runtime property verification processes an execution trace (101) containing the sequence of runtime events captured from a monitored embedded system. The key attributes (102) represent the selected system variables (x₁, ..., xₙ) to be tracked for property verification. The linear state model construction (103) processes the execution trace to generate a linear state model (LSM) (104) that records every state change in temporal order. The distinct state model construction (105) eliminates duplicate states to create a distinct state model (DSM) (106). Abstraction functions (107) including Boolean (111), Multi-valued (112), and Path (113) abstractions are applied during abstract model construction (108) to generate an abstract state model (ASM) (109). Finally, property verification (110) is performed on the abstract model to check safety properties.
[0029] In an embodiment, the execution trace (101) in the system (100) represents a comprehensive log of runtime events captured during system execution. The execution trace (101) contains a temporal sequence of all relevant state changes, including variable assignments, method calls, and control flow transitions. Each event in the trace (101) includes information about which variables changed, their new values, and the time of occurrence. The execution trace (101) serves as the primary input for all subsequent model construction stages. The trace (101) can be captured through various instrumentation techniques, with the actual capture mechanism potentially implemented in hardware as depicted in Figure 6.
[0030] In an embodiment, the key attributes (102) represent the carefully selected subset of system variables chosen for monitoring and verification. These attributes (102) typically include safety-critical variables such as sensor readings, actuator commands, and control state indicators. The selection of key attributes (102) is crucial as it determines both the accuracy of the verification and the size of the resulting models. Each key attribute in the set (x₁, ..., xₙ) corresponds to a specific system variable whose value changes are tracked throughout the execution. The key attributes (102) form the state vector used in all subsequent model construction phases.
[0031] In an embodiment, the linear state model construction (103) processes the execution trace (101) sequentially to build a linear state model (LSM) (104). This construction process (103) creates a new state for every event in the execution trace that modifies any key attribute. The resulting LSM (104) preserves the exact temporal ordering of all state changes, creating a linear sequence of states connected by transitions. The size of the LSM (104) is directly proportional to the length of the execution trace. While this model provides the most accurate representation of system behavior, it can become very large for long-running executions.
[0032] In an embodiment, the distinct state model construction (105) processes the linear state model (104) to identify and merge duplicate states. States are considered duplicates when they have identical values for all key attributes (102). The construction process (105) creates a distinct state model (DSM) (106) containing only unique states. This merging process can significantly reduce the model size, especially for systems that revisit the same states multiple times. However, the DSM (106) may contain additional paths between states that were not directly connected in the original LSM (104), as multiple linear paths may converge to the same distinct state.
[0033] In an embodiment, the distinct state model (DSM) (106) represents a compressed version of the linear state model where each unique combination of key attribute values appears only once. The DSM (106) maintains transition information showing which states can reach which other states, though the temporal ordering information from the LSM is partially lost. The DSM (106) is particularly useful for checking state-based properties that don't depend on specific execution paths. The model size reduction achieved by the DSM (106) depends on the repetitiveness of the system behavior - systems with cyclic behavior show greater reduction.
[0034] In an embodiment, the abstraction functions (107) provide systematic methods for mapping concrete domain values to abstract domains. These functions include Boolean abstractions (111) that map values to true/false based on predicates, multi-valued abstractions (112) that partition value ranges into multiple categories, and path abstractions (113) that abstract control flow sequences. Each abstraction function is designed to preserve specific properties while reducing the state space. The choice of abstraction function (107) depends on the property to be verified and the nature of the key attributes being abstracted.
[0035] In an embodiment, the abstract model construction (108) applies the selected abstraction functions (107) to transform the distinct state model (106) or linear state model (104) into an abstract state model (ASM) (109). This construction process (108) replaces concrete values with their abstract representations, potentially merging many concrete states into single abstract states. The process ensures that the resulting abstract model preserves the properties of interest while achieving significant state space reduction. The construction (108) must carefully handle transitions to ensure the abstract model correctly represents possible behaviors of the concrete system.
[0036] In an embodiment, the abstract state model (ASM) (109) represents the final reduced model used for property verification. The ASM (109) contains abstract states where each component of the state vector has been replaced by its abstraction. The model achieves compression ratios of 100-1000x compared to concrete state storage while preserving property-relevant information. The ASM (109) maintains transition relations between abstract states, enabling both state-based and path-based property verification. The size and complexity of the ASM (109) depend on the abstraction functions chosen and the inherent complexity of the system behavior.
[0037] In an embodiment, the property verification (110) process evaluates safety properties on the abstract state model (109). For state-based properties using the G (globally) operator, verification checks that the property holds in every reachable abstract state. For path-based properties using the P operator, verification examines paths through the abstract model. The verification process (110) must account for the abstraction by checking that abstract states satisfy the property for all concrete states they represent. The verification results are sound - if a property is verified on the abstract model, it holds for the concrete system.
[0038] In an embodiment, the Boolean abstraction (111) represents one of the fundamental abstraction types available in the system. Boolean abstraction maps concrete values to binary abstract values based on predicates such as x > c, x = c, or x < c for some constant c. This abstraction is particularly useful when properties depend only on whether values fall within certain ranges rather than exact values. Boolean abstraction achieves maximum compression, reducing any concrete domain to just two abstract values, while preserving properties that can be expressed as Boolean conditions over the concrete values.
[0039] In an embodiment, the multi-valued abstraction (112) extends Boolean abstraction by partitioning concrete domains into multiple abstract values. A common form is range abstraction [c₁:c₂:...:cₙ] which creates n+1 abstract values corresponding to the intervals defined by the constants. This abstraction type provides finer granularity than Boolean abstraction while still achieving significant state space reduction. Multi-valued abstraction is useful for properties that distinguish between multiple operational regions or modes of the system.
[0040] In an embodiment, the path abstraction (113) operates on control flow sequences rather than data values. This abstraction type is particularly relevant for control-oriented properties that specify required or forbidden execution sequences. Path abstraction identifies key control points (such as method entries or specific statements) and abstracts away intermediate execution steps. The resulting abstract model preserves paths between these key points while eliminating irrelevant intermediate states.
[0041] In an embodiment, referring to FIG. 2, the system architecture (200) comprises both software and hardware layers. The software layer contains the model construction and verification algorithms, including the execution trace processing, state model construction, and abstraction applications. The hardware layer, detailed in FIG. 6, provides acceleration support through FPGA-based event capture and ASIC-based verification processing. This layered architecture allows the conceptual model construction process to be implemented efficiently with hardware acceleration where needed.
[0042] In an embodiment, referring to FIG. 3, the property verification process (300) on abstract state models employs different strategies based on the property type. For state-based properties specified with the G[p] operator, the process performs state-based checking, evaluating whether property p holds in each abstract state. The verification must consider that each abstract state represents multiple concrete states. For path-based properties specified with the P operator, the process performs path-based checking, examining sequences through the abstract model. The choice between Boolean, multi-valued, or path abstraction affects the verification approach.
[0043] In an embodiment, the actuator commands (615a) identified within safety-critical variables can represent control outputs affecting physical system behavior. The commands (615a) can include motor torque settings, valve positions, and brake force values. The actuator commands can directly influence system safety requiring careful monitoring. The commands (615a) can be bounded by physical constraints encoded in safety properties. The actuator values can be abstracted into safe, warning, and dangerous zones for efficient verification.
[0044] In an embodiment, the sensor readings (616a) can provide environmental and system feedback essential for control decisions. The readings (616a) can include position sensors, pressure transducers, and temperature monitors. The sensor values can indicate system operating conditions affecting safety margins. The readings (616a) can be validated against expected ranges detecting sensor failures. The sensor data can be abstracted based on operational regions simplifying verification. The sensor information can correlate with actuator commands validating control laws.
[0045] In an embodiment, the control variables (609-612) can encompass specific control parameters critical for system operation. The speed control variable (609) can monitor velocity setpoints and actual speeds. The position control variable (610) can track spatial coordinates and trajectories. The temperature control variable (611) can regulate thermal parameters within safe operating ranges. The pressure control variable (612) can maintain hydraulic or pneumatic system pressures. Each control variable can be independently monitored and abstracted for efficient verification.
[0046] In an embodiment, the control state variables (617a) can track program execution state and mode transitions. The variables (617a) can include finite state machine states, operation modes, and error flags. The control states can determine which safety properties apply at different execution phases. The state variables (617a) can be encoded efficiently using enumerated types. The control flow information can enable path-based property verification. The state tracking can detect illegal mode transitions violating safety specifications.
[0047] In an embodiment, referring to FIG. 4, the control-oriented abstraction (400) provides hierarchical levels for analyzing system execution. The execution trace containing control events (101) flows through control attribute extraction (401) which identifies package, class, method, and thread information. The abstraction level decision (402) determines whether to use package-level (403), class-level (404), method-level (405), or thread-level (406) abstraction. These different levels create control-oriented models (407) with varying granularity. Additionally, path abstraction (113) can be applied for property-specific verification scenarios.
[0048] In an embodiment, the hardware comparator arrays (822) within parallel verification engines can evaluate logical implications (635) between characteristic functions and properties. The arrays (822) can implement fast comparison operations using specialized circuits. The comparators can detect property satisfaction or violation within single cycles. The arrays (822) can process vector comparisons for multi-variable properties. The hardware implementation can eliminate software comparison overhead. The comparator results can feed interrupt generation logic.
[0049] In an embodiment, the abstract state vectors (623) generated by the model construction engine can represent system state using compressed bit patterns (625). The vectors (623) can encode each safety-critical variable's abstract value using minimal bits. The state representation can achieve 100-1000x compression compared to concrete storage. The vectors (623) can be stored efficiently in cache memory supporting large state spaces. The abstract encoding can preserve all safety-relevant information while discarding irrelevant details. The state vectors can be compared efficiently using hardware operations.
[0050] In an embodiment, the compressed bit patterns (625) can encode abstract zone membership using efficient binary representations. The patterns (625) can use as few as two bits for binary abstractions or multiple bits for multi-valued zones. The compression can achieve two orders of magnitude reduction in storage requirements. The bit patterns can be packed into machine words enabling efficient processing. The compressed representation can support fast comparison and lookup operations. The patterns (625) can be decoded when needed for property evaluation or debugging.
[0051] In an embodiment, the state transition graphs (626) maintained within the verification processor (110) as part of the abstract model construction engine can capture temporal evolution of abstract system state. The graphs (626) can represent states as nodes and transitions as edges triggered by events. The transition graphs can be built incrementally as new states are discovered. The graphs (626) can include transition counts for probabilistic analysis. The graph structure can enable efficient reachability analysis and cycle detection. The transition information can support temporal property verification beyond state-based checks.
[0052] In an embodiment, the safety property specifications (617b) processed by transformation circuits can define forbidden control states (628) that must never occur. The specifications (617b) can be expressed using formal notation or domain-specific languages. The properties can include state invariants, temporal constraints, and safety envelopes. The specifications (617b) can be validated for consistency before transformation. The property definitions can reference abstract rather than concrete values simplifying expression. The specifications can be provided by safety engineers or derived from standards.
[0053] In an embodiment, the hardware-verifiable conditions (618) output by transformation circuits can directly execute on verification hardware. The conditions (618) can be expressed as Boolean circuits evaluating abstract state vectors. The hardware form can eliminate interpretation overhead achieving maximum performance. The conditions (618) can be optimized through logic synthesis reducing gate count. The verifiable format can support parallel evaluation of multiple properties. The hardware conditions can include both combinational and sequential elements.
[0054] In an embodiment, the characteristic function circuits (619) can implement membership tests for abstract value sets. The circuits (619) can use multiplexer arrays (629) selecting outputs based on abstract values. The characteristic functions can output logic high when values belong to specified sets. The circuits (619) can be generated automatically from property specifications. The multiplexer-based implementation can achieve single-cycle evaluation. The characteristic functions can be combined to form complex property expressions.
[0055] In an embodiment, the verification logic networks (630) can combine characteristic function outputs to evaluate complete properties. The networks (630) can use AND gates (631) for conjunctions and OR gates (632) for disjunctions. The logic networks can implement arbitrary Boolean expressions over abstract values. The networks (630) can be optimized through standard logic minimization techniques. The verification logic can include temporal elements for sequence detection. The network outputs can directly trigger violation responses.
[0056] In an embodiment, the interrupt signal generator (828) within property transformation circuits can produce hardware interrupts upon property violations (633). The generator (828) can interface with system interrupt controllers ensuring immediate response. The interrupt signals can have programmable priorities based on property criticality. The generator (828) can include deglitching logic preventing spurious triggers. The interrupt mechanism can achieve microsecond-level response times. The hardware interrupts can trigger safety shutdown procedures protecting system integrity.
[0057] In an embodiment, the parallel verification engine (605) can evaluate multiple abstract states against properties simultaneously. The engine (605) can be implemented as a pipelined architecture (634) within the ASIC. The parallel design can include multiple state evaluation units (620) operating independently. The engine (605) can achieve throughput of one verification per clock cycle. The parallel architecture can scale with additional evaluation units. The verification engine can maintain deterministic timing supporting real-time guarantees.
[0058] In an embodiment, the multiple state evaluation units (620) within parallel engines can process different abstract states (623) concurrently. Each unit (620) can include dedicated logic for property evaluation against assigned states. The evaluation units can operate without mutual interference enabling linear scaling. The units (620) can be dynamically assigned states based on workload. The parallel evaluation can reduce worst-case verification latency proportionally. The state evaluation units can share property circuits through multiplexing.
[0059] In an embodiment, the hardware comparator arrays (622) can evaluate logical implications (635) between characteristic functions and properties. The arrays (622) can implement fast comparison operations using specialized circuits. The comparators can detect property satisfaction or violation within single cycles. The arrays (622) can process vector comparisons for multi-variable properties. The hardware implementation can eliminate software comparison overhead. The comparator results can feed interrupt generation logic.
[0060] In an embodiment, the interrupt generation unit (823) can coordinate responses to property violations across parallel evaluators. The unit (823) can prioritize multiple simultaneous violations based on criticality. The interrupt generation can include event logging for post-analysis. The unit (823) can trigger safety shutdown procedures (637) protecting system state. The interrupt mechanism can interface with controller safety systems. The generation unit can support configurable response strategies.
[0061] In an embodiment, the system (100) can achieve real-time verification with latency below one millisecond for control systems operating at frequencies up to one kilohertz. The verification performance enables deployment in safety-critical automotive braking systems, industrial robot controllers, and aircraft flight control systems. The abstraction-based approach reduces verification requirements by at least two orders of magnitude compared to concrete state monitoring, making implementation feasible for resource-limited embedded platforms. The actual hardware implementation supporting these performance characteristics is detailed in Figure 6.
[0062] FIG. 2 illustrates an exemplary schematic representation of the runtime verification architecture (200) showing the complete system organization. The architecture comprises a software layer containing the Java application (201), JVM (202), BCI Agent (203) with bytecode transformer (204) and event handler (205), inclusion filter (206), and online verification module (210). The hardware layer includes the target embedded controller (102) and verification hardware consisting of FPGA and ASIC chips. The architecture demonstrates how execution events flow from the monitored application through various processing stages to achieve real-time verification with sub-millisecond latency.
[0063] FIG. 3 illustrates an exemplary representation of the property verification process (300) on abstract state models. Starting with an abstract state model (ASM), the system determines the property type - either G[p] for state-based properties or P[...] for path-based properties. State-based checking (Algorithm 4/5) verifies that property p holds in all abstract states, while path-based checking (Algorithm 6) examines paths through the model. The verification process produces either a verified result (306) or identifies counterexamples (307). The choice of abstraction type (Boolean, multi-valued, or path) affects the verification algorithm used.
[0064] FIG. 4 illustrates an exemplary representation of control-oriented abstraction (400) for runtime verification. The process begins with an execution trace (101) containing control events, which flows to a control attribute module (401) for extracting package/class/method information. An abstraction level decision point (402) determines the appropriate granularity. The hierarchical abstraction levels include package-level abstraction (403) for high-level flow between packages, class-level abstraction (404) for inter-class interactions, method-level abstraction (405) for detailed method-level analysis, and thread-level abstraction (406) for concurrent execution analysis. These abstractions generate a control-oriented model (407) with reduced state space. Path abstraction (113) provides an alternative approach for property-specific verification
[0065] In an embodiment, referring to FIG. 4, the abstraction system begins with an execution trace (101) containing control events which flows to a control attribute module (401) for extracting package/class/method information. The system implements an abstraction level decision point (402) that determines the appropriate granularity of abstraction based on the verification requirements. The hierarchical abstraction levels include package-level abstraction (403) operating on package hierarchies p1.p2.p3, class-level abstraction (404) targeting class instances p.c.i, method-level abstraction (405) focusing on method executions c.m(), and thread-level abstraction (406) based on thread identifiers. All hierarchical abstractions converge to generate a control-oriented model (407) with significantly reduced state space compared to concrete models. Additionally, the system supports direct path abstraction (113) through Algorithm 3 for property-specific verification scenarios, enabling efficient verification of temporal properties while maintaining property preservation guarantees across the abstraction hierarchy.
[0066] FIG. 5 illustrates an exemplary representation of the abstract state model construction process (500). Starting with an execution trace (101) containing field write events and key attributes (102) selected for monitoring, the process constructs state vectors (501). An abstraction type decision (502) determines whether to apply Boolean (111), multi-valued (112), or subgraph (503) abstraction. The selected abstraction transforms the concrete state vectors into abstract representations, ultimately producing an abstract state model (109) with reduced state space while preserving properties relevant for verification.
[0067] FIG. 6 illustrates an exemplary block diagram depicting the integration of hardware instrumentation interface, application-specific integrated circuit, and cache memory components, in accordance with an embodiment of the present disclosure.
[0068] In an embodiment, referring to FIG. 6 illustrating the integrated system architecture (600) depicting component interconnections and data flow paths. The hardware instrumentation interface (101) with FPGA (103) connects to the target embedded controller (102) monitoring control variables including speed control (609), position control (610), temperature control (611), pressure control (612), actuator commands (615a), sensor readings (616a), and control state variables (617a). The FPGA communicates with the ASIC through DMA channel (608) enabling high-speed data transfer (603). The ASIC (111) integrates the verification processor (110) with abstract model construction (613), abstraction circuits (614), and state transition graphs (626); property transformation circuit (604) with safety properties (617b) converting to hardware conditions (618) through characteristic functions (619) and interrupt generator (828); and parallel verification engine (605) with multiple state evaluators (620), hardware comparator arrays (822), interrupt generation unit (823), latency monitor (624), and throughput counter (625) in pipelined architecture (634). The cache memory (112) interfaces with all processing elements through high-bandwidth internal buses. The integrated design minimizes communication latency achieving sub-millisecond end-to-end verification response times (601) supporting real-time property checking requirements.
[0069] FIG. 7 illustrates an exemplary flow diagram depicting a method for abstraction-based runtime property verification, in accordance with an embodiment of the present disclosure.
[0070] In an embodiment, referring to FIG. 7 illustrating a method for abstraction-based runtime property verification (700). The method begins at step (702) with intercepting memory write operations through hardware mechanisms and generating event data packets that form the execution trace. At step (704), the method executes abstract model construction by processing the execution trace to extract key attributes and apply selected abstraction functions to generate abstract state vectors with compressed representations. The abstract model construction can be performed directly on the execution trace without requiring intermediate linear or distinct state model construction, thereby reducing computational overhead when such intermediate models are not necessary for the specific verification requirements. At step (706), the method transforms safety property specifications into verifiable conditions suitable for evaluation on abstract models. Finally, at step (708), the method executes property verification using appropriate algorithms based on the property type and abstraction used.
[0071] In an embodiment, the method step (702) for intercepting memory write operations at hardware level can involve configuring FPGA (103) logic to monitor specific memory address ranges. The FPGA can detect write transactions on the memory bus within single clock cycles and generate event data packets, wherein each event data packet comprises a memory address of a modified field, a data value written to the memory address, and a hardware timestamp. The hardware-level monitoring can operate transparently without modifying target controller (102) software. The captured operations can be filtered based on relevance to safety properties reducing processing overhead.
[0072] In an embodiment, the method step (704) for executing abstract model construction can involve receiving event data packets through direct memory access channels (603). The construction engine can extract control variables from the event data packets by filtering memory addresses against predefined patterns. The engine can apply hardware-optimized abstraction circuits that partition concrete sensor value ranges into abstraction types (111, 112, 113) through comparator circuits implementing threshold detection. The abstract state vectors can be generated by encoding concrete values into compressed bit patterns representing said abstraction types, thereby reducing memory consumption by a factor of at least one hundred. The state transition graphs can be established by detecting changes in the compressed bit patterns between consecutive event data packets.
[0073] In an embodiment, the method step (706) for transforming safety property specifications into hardware-verifiable conditions can involve parsing safety property specifications through at least one property transformation circuit (604) implemented using combinational logic gates within the application-specific integrated circuit (111). The transformation circuit can implement characteristic function circuits through multiplexer arrays encoding zone membership tests. The circuit can construct verification logic networks that combine outputs through logic gates including Boolean gates for conjunctions and disjunctions. The hardware implementation can achieve single-cycle property evaluation latency. The transformed conditions can support both state invariants and temporal properties.
[0074] In an embodiment, the parallel verification engine (605) can incorporate performance monitoring components for real-time diagnostics. The latency monitor (624) can measure verification cycle times ensuring sub-millisecond response requirements are met. The throughput counter (625) can track the number of states verified per second, validating the system's ability to process over ten thousand states per second. These monitoring components can provide runtime feedback on verification performance enabling dynamic optimization of resource allocation.
[0075] In an embodiment, the method step (708) for executing parallel verification engines can involve operating multiple state evaluation units in parallel wherein each evaluates different abstract states simultaneously. The engines can evaluate states against hardware-verifiable conditions in parallel pipelines within the pipelined architecture. The hardware comparators can check logical implications within single clock cycles. The interrupt generation units can trigger immediate safety responses upon violation detection. The parallel architecture can sustain verification throughput matching event generation rates ensuring no verification backlog and achieving real-time verification with latency below one millisecond (601) for control systems operating at frequencies up to one kilohertz.
[0076] The described disclosure presents an advanced abstraction-based runtime property verification system (100) that systematically constructs abstract models from execution traces. The system can achieve real-time verification with latency below one millisecond for control systems operating at frequencies up to one kilohertz, enabling deployment in safety-critical automotive braking systems, industrial robot controllers, and aircraft flight control systems. The abstraction-based approach can reduce verification requirements by at least two orders of magnitude compared to concrete state monitoring.
[0077] The described disclosure presents an advanced abstraction-based runtime property verification system (100) that employs systematic model construction and abstraction techniques. The system can process execution traces to construct linear state models, eliminate duplicates to form distinct state models, and apply various abstraction functions to create compact abstract models suitable for efficient property verification. The verification process can handle both state-based properties using the G operator and path-based properties using the P operator. When combined with hardware acceleration as shown in Figure 6, the system enables real-time verification in resource-constrained embedded environments.
[0078] In an exemplary embodiment, the system (600) can operate within validated performance parameters ensuring reliable property verification across safety-critical applications. The system (600) can demonstrate verification latency below one millisecond for control frequencies up to one kilohertz through hardware optimization. The abstraction mechanism can achieve state space reduction exceeding two orders of magnitude with property preservation. The parallel verification can process over ten thousand states per second with dedicated ASICs. The system (600) can operate continuously within embedded controller power budgets supporting permanent deployment. These validated performance metrics establish the system (600) as practical, efficient, and scalable for diverse safety-critical embedded applications requiring runtime verification assurance.
[0079] In an embodiment, the reference numerals shown in the accompanying drawings represent the components of the abstraction-based runtime property verification system. In Figures 1-5, the components depict the software-based model construction and verification process: Execution Trace (101) represents the captured runtime events; Key Attributes (102) are the monitored variables; Linear State Model Construction (103) and the resulting LSM (104); Distinct State Model Construction (105) and DSM (106); Abstraction Functions (107) including Boolean (111), Multi-valued (112), and Path (113) types; Abstract Model Construction (108) and the resulting ASM (109); and Property Verification (110). Figure 6 separately illustrates the hardware acceleration architecture with components including the Target Embedded Controller (102), FPGA (103), ASIC (111), Verification Processor (110), and related hardware elements. Figure 7 shows the method steps (702, 704, 706, 708) for the verification process
[0080] While the foregoing describes various embodiments of the proposed disclosure, other and further embodiments of the proposed disclosure may be devised without departing from the basic scope thereof. The scope of the proposed disclosure is determined by the claims that follow. The proposed disclosure is not limited to the described embodiments, versions or examples, which are included to enable a person having ordinary skill in the art to make and use the invention when combined with information and knowledge available to the person having ordinary skill in the art.

ADVANTAGES OF THE PRESENT DISCLOSURE
[0081] The present disclosure enables transparent hardware-level monitoring without modifying target controller software, ensuring uninterrupted operation of safety-critical embedded systems during active property verification.
, Claims:1. A system (100) for abstraction-based runtime property verification, the system comprising:
an execution trace (101) containing runtime events captured from a target embedded controller through a hardware instrumentation interface;
a set of key attributes (102) representing monitored system variables selected for verification;
a linear state model construction process (103) executable on at least one processor that generates a linear state model (LSM) (104) capturing temporal sequences of state changes from said execution trace;
a distinct state model construction process (105) executable on said processor that eliminates duplicate states from the linear state model to generate a distinct state model (DSM) (106);
abstraction functions (107) implemented in hardware-optimized circuits, wherein the abstraction functions include Boolean abstraction (111), Multi-valued abstraction (112), and Path abstraction (113) that partition concrete value ranges into abstract domains through comparator circuits implementing threshold detection;
an abstract model construction process (108) executed on at least one dedicated verification processor (110) implemented on at least one application-specific integrated circuit (111) that applies said abstraction functions to generate an abstract state model (ASM) (109), reducing memory consumption by a factor of at least one hundred;
a property verification process (110) executed on said verification processor that evaluates state-based and path-based safety properties on the abstract state model;
a property transformation circuit (604) implemented on said application-specific integrated circuit that transforms safety property specifications into hardware-verifiable conditions;
a parallel verification engine (605) implemented as a pipelined architecture on said application-specific integrated circuit comprising multiple state evaluation units operating in parallel for simultaneous property evaluation;
wherein the system achieves real-time verification with latency below one millisecond for control systems operating at frequencies up to one kilohertz, and the abstraction-based approach reduces verification hardware requirements by at least two orders of magnitude compared to concrete state monitoring.
2. The system as claimed in claim 1, wherein the abstraction functions (107) implemented in hardware-optimized circuits comprise:
boolean abstraction (111) implemented through comparator logic that maps concrete values to binary abstract values based on threshold comparison; and
multi-valued abstraction (112) implemented through multiple comparator stages that partition concrete values into three or more abstract zones through cascaded threshold detection.
3. The system as claimed in claim 1, wherein the abstract model construction process (108) executed on the verification processor (110):
identifies control flow states from the execution trace (101) by detecting control events corresponding to program execution points; and
collapses sequences of state transitions into single abstract transitions when intermediate states do not affect safety properties.
4. The system as claimed in claim 1, further comprising:
a hardware instrumentation interface including at least one field programmable gate array (103) that intercepts memory write operations at hardware level and generates event data packets forming the execution trace (101);
wherein each event data packet comprises a memory address of a modified field, a data value written to the memory address, and a hardware timestamp.
5. The system as claimed in claim 1, wherein the property transformation circuit (604):
receives safety property specifications containing temporal operators;
implements characteristic function circuits through multiplexer arrays encoding abstract value membership tests; and
constructs verification logic networks that combine outputs through AND and OR gates for property evaluation.
6. The system as claimed in claim 1, further comprising:
a direct memory access channel (603) enabling high-speed transfer of event data from the hardware instrumentation interface to the verification processor (110);
cache memory (112) storing the abstract state model (109) and executable instructions for model construction and verification processes.
7. The system as claimed in claim 1, wherein:
the hardware instrumentation interface selectively captures memory write operations based on address ranges specified in a configuration register corresponding to the key attributes (102); and
stores event data packets in at least one circular first-in-first-out memory buffer when verification processing experiences temporary delays.
8. The system as claimed in claim 1, wherein the verification processor (110):
extracts abstract state vectors from the abstract state model (109) stored in cache memory; and
generates verification results indicating property satisfaction or violation with counterexample paths when violations are detected.
9. The system as claimed in claim 5, wherein the property transformation circuit (604):
processes state-based safety properties by generating hardware circuits that evaluate whether specified conditions hold in each abstract state throughout system execution;
processes path-based safety properties by generating circuits that verify all execution paths from states satisfying a first condition to states satisfying a third condition pass through states satisfying a second condition; and
separates complex properties into conjunctions of simpler properties for parallel evaluation by the multiple state evaluation units
10. A method (700) for abstraction-based runtime property verification, the method comprising:
intercepting (702) memory write operations at hardware level through at least one field programmable gate array integrated with a target embedded controller and generating event data packets forming an execution trace (101), wherein each event data packet comprises a memory address of a modified field, a data value written to the memory address, and a hardware timestamp;
executing (704) model construction processes on at least one dedicated verification processor implemented on at least one application-specific integrated circuit, wherein executing comprises:
processing the execution trace (101) to identify key attributes (102);
constructing a linear state model (104) through a linear state model construction process (103);
generating a distinct state model (106) through a distinct state model construction process (105) that eliminates duplicate states;
applying hardware-optimized abstraction functions (107) including Boolean (111), Multi-valued (112), and Path (113) abstractions that partition concrete value ranges into abstract domains;
generating an abstract state model (109) through an abstract model construction process (108), thereby reducing memory consumption by a factor of at least one hundred;
transforming (706) safety property specifications into hardware-verifiable conditions through at least one property transformation circuit implemented using combinational logic gates within the application-specific integrated circuit, wherein transforming comprises constructing verification logic networks that combine outputs through logic gates;
executing (708) at least one parallel verification engine implemented as a pipelined architecture within the application-specific integrated circuit to verify state-based and path-based safety properties on the abstract state model, wherein executing comprises operating multiple state evaluation units in parallel wherein each evaluates different abstract states simultaneously;
wherein the method achieves real-time verification with latency below one millisecond for control systems operating at frequencies up to one kilohertz.