PaperlayerView exact revision on arXiv

Source-linked AI summary

Constraint-Driven Modeling Enabling Dual Model Checking and Simulation for Discrete Event Systems

Soroosh Gholami, Hessam S. Sarjoughian

arXiv:2608.22095v1cs.SEcs.ARcs.LO

TL;DR

The paper addresses the difficulty of model checking DEVS models alongside simulation because of continuous time and unbounded state spaces. It introduces Constraint-DEVS within DEVS-Suite to support model checking and simulation, demonstrated through Network-on-Chip models and comparisons with UPPAAL.

  • Problem

    Continuous time and boundless state spaces make DEVS model checking difficult, despite DEVS models being well-suited for simulation.

  • Method

    Constraint-DEVS extends DEVS-Suite with bounded models, a state exploration protocol, and support for verification alongside simulation.

  • Results

    The work creates Network-on-Chip models and contrasts their modeling, simulation, and model-checking treatment in UPPAAL and DEVS-Suite.

  • Takeaways & Limitations

    DEVS-Suite supports both verification through model checking and validation through simulation within the presented framework.

  • Takeaways & Limitations

    The comparison is limited to the selected environments, although other realizations exist.

Abstract

from arXiv · show

Verification and validation (V&V) are crucial methods for evaluating the requirements and specifications of dynamical models that fulfill their intended purposes. Parallel Discrete EVent System Specification (PDEVS) is a system-theoretic modeling approach for creating modular, hierarchical component-based simulation models. In this paper, we introduce Constraint-DEVS, a method for creating bounded Parallel DEVS models that lend themselves, in addition to simulation, to model checking. We extend the DEVS-Suite framework to create Constraint-DEVS specifications which can then be model checked using a proposed state exploration protocol with the Parallel DEVS abstract simulator protocol. These capabilities, along with the support for non-determinism, complex data transfer, and performance-related property checking, make Constraint-DEVS and its accompanying DEVS-Suite a unique framework for the development, verification, and validation of discrete-event systems. In order to demonstrate this work, we developed and verified models of Network-on-Chip. Also, we detail behavioral design artifacts for the DEVS-Suite framework's hybrid model-checking and simulation engine.

1 INTRODUCTION

The introduction frames simulation as validation and model checking as verification, then presents Constraint-DEVS and DEVS-Suite as a way to support both for bounded discrete-event models. It demonstrates the approach with Network-on-Chip models and compares DEVS-Suite with UPPAAL for complex-system modeling, simulation, and checking.

  • 1 INTRODUCTION: Designers use simulation and model checking together to evaluate whether dynamical models satisfy intended requirements and specifications.Simulation is presented as validation, while model checking is presented as verification.
  • 1 INTRODUCTION: State explosion complicates model checking, while standard DEVS models have continuous time and unbounded state spaces that hinder checking.A bounded state space is necessary for model checking.
  • 1 INTRODUCTION: Constraint-DEVS is introduced as a contribution enabling DEVS-Suite to support model checking alongside simulation.The paper extends the framework to support Constraint-DEVS modeling and verification via model checking.
  • 1 INTRODUCTION: The paper develops Network-on-Chip models in Constraint-DEVS and verifies NoC-specific properties using DEVS-Suite.These models demonstrate the environment's combined modeling, simulation, and model-checking capability.
  • 1 INTRODUCTION: A comparable UPPAAL model using Timed Automata is developed to contrast the two environments' modeling, simulation, and model-checking capabilities.The comparison is limited to UPPAAL and DEVS-Suite, although other realizations exist.

2 BACKGROUND

DEVS models specify communicating atomic and coupled components for simulation, while Constraint-DEVS extends this setting toward bounded-state model checking. The section illustrates these ideas through a NoC circular buffer and a DEVS-Suite execution protocol that can support exploration.

  • DEVS Modeling: DEVS represents models through atomic state and transition functions, plus coupled structures that organize component communication hierarchically.Atomic models define external, internal, confluent, output, and time-advance behavior; coupled models specify components and their couplings.
  • DEVS Modeling: A NoC circular buffer models flit storage with separate input and trigger ports, one output port, FIFO behavior, and bounded-operation assumptions.The model stores incoming flits, outputs the queue head after a trigger, and disallows insertion into a full buffer or retrieval from an empty buffer.
  • DEVS Modeling: The ordinary DEVS circular-buffer model is suitable for simulation only, whereas its Constraint-DEVS realization is intended for both model checking and simulation.The Constraint-DEVS version is presented as a later extension of the simulation-only Listing 1 model.
  • DEVS Simulation: The model-checking extension wraps the DEVS-Suite simulation protocol in a state-exploration protocol for cycle-by-cycle execution.The paper identifies bounded state space as necessary for model checking and incorporates the simulation engine into the model-checking engine.
  • DEVS Simulation: DEVS-Suite simulation uses simulator and coordinator protocols to manage timing, select transition functions, and exchange events across atomic and coupled models.Execution compares event time with the next scheduled event, invokes output before internal transition when applicable, and then schedules the next event.
  • DEVS Simulation: The proposed environment targets Constraint-DEVS modeling and verification with support for nondeterminism, stochasticity, complex data transfer, and broader property checking.The stated goal is to extend DEVS-Suite beyond the capabilities supported by LTL and CTL alone.

3 RELATED WORK

Prior DEVS-based verification approaches enable model checking through model conversion but remain limited in complex data, structural modeling, and property expressiveness. Constraint-DEVS instead targets integrated simulation and verification while preserving DEVS modeling capabilities.

  • Existing limitations: Petri nets and Time Automata support concurrent-system behavior but cannot readily represent complex data types or system structure.These methods model behaviors of concurrent systems rather than the structure of a given system.
  • Property expression: LTL, CTL, and CTL* are insufficient for complex QoS properties such as average packet latency over time.The discussion distinguishes these temporal properties from state-based properties evaluated at one time instance.
  • DEVS-based approaches: FD-DEVS, RTA-DEVS, and FPDEVS require conversion to PROMELA, Time Automata, or related verification representations.The converted models are verified with tools such as SPIN or UPPAAL.
  • DEVS-based approaches: Converted DEVS approaches retain limitations in complex data, structural modeling, and tree-logic property expression.Their property languages do not adequately express complex properties described in the related-work discussion.
  • Positioning: Constraint-DEVS aims to enable state-exploration verification while retaining simulation functionality for formal Network-on-Chip modeling.This goal differs from a related Cellular Automata framework focused primarily on fast modeling and simulation.
  • Verification challenge: Model checking faces state explosion, making verification of large hybrid systems impractical and motivating simulation- and falsification-based approaches.The paper positions its tool as supporting both simulation and model checking of dynamic models.

4 CONSTRAINT-DEVS

Constraint-DEVS bounds states, inputs, events, and time so DEVS models have finite spaces suitable for exhaustive exploration. Its protocol combines controlled simulation with reachability analysis and selective state representation.

  • Requirements: Model verification adds bounded state and input configurations, finite internal and external events, and a state exploration protocol.These four capabilities are identified as requirements for verification within the DEVS framework.
  • Bounded specifications: Regular expressions specify finite primitive and compound state spaces, allowing the exploration protocol to calculate and enumerate combinations.Compound variables can represent structures such as fixed-size queues.
  • Bounded specifications: External input ports use bounded value sets with an added NULL value, and the verifier applies all possible input combinations to reachable states.Internal input and output ports remain driven by the model's internal components.
  • Time and events: Discrete time and delayed external events restrict transition instances so the model retains a finite state space.The time-advance function uses a finite set of values, while external events are processed at discrete time instances.
  • State exploration: The exploration protocol repeatedly removes a state from Q, applies possible inputs, executes one simulation cycle, and records visited or unsafe states.Simulation is embedded within model checking as controlled one-cycle execution.
  • Selective state representation: Explorable variables contribute distinct states to verification, whereas unexplorable variables remain operationally active but their changes are ignored by the verification engine.This distinction supports selective control over the collective state-space size.
  • Selective state representation: For a network of 6 nodes, the queue state space is given as 6^8 ≈ 1M, illustrating the rapid growth caused by packet combinations.The example uses a queue capacity of 8 and 100 possible packet values.

4.5 Trace Analysis

Constraint-DEVS builds a reachability graph during exhaustive exploration and analyzes it through states, paths, subtrees, or pruned traces. DEVS-Suite implements these capabilities for verification and validation.

  • Reachability analysis: The verifier explores the reachable state space from initial states while a transducer records nodes as states and edges as transitions.The resulting reachability graph can be analyzed after exploration.
  • Trace analysis: Pruning cycles converts the reachability graph into traces suitable for checking state-, path-, and subtree-based properties.The paper illustrates these trace forms using two initial states.
  • State-space reduction: Data exclusion removes verification-irrelevant data to reduce the explored state-space size.The method is identified as selective state exploration.
  • Property checking: Experimental Frames provide generator and transducer components for exploring state spaces and collecting traces without relying only on LTL or CTL.The EF is implemented as a non-DEVS component.
  • Implementation: Constraint-DEVS and its verification features are realized in DEVS-Suite.The implementation extends the framework while supporting the described modeling and checking workflow.

5 CIRCULAR BUFFER EXAMPLE

The circular-buffer example demonstrates how Constraint-DEVS models are specified, exhaustively verified, and instrumented with transducers. It also exposes the computational cost of growing state spaces.

  • Model specification: The circular buffer models head, tail, and buffer-status variables with trigger and flit input ports.The buffer capacity is 8, and flits are represented as 24-bit values.
  • State exploration: A 100-node network with 99 destinations produces 12,600 state-events for the circular-buffer verification model.The count combines state and input-event possibilities.
  • Verification instrumentation: The generated verification model records inputs, buffer state, and outputs for subsequent analysis.DEVS-Suite automatically generates the generator and verification engine.
  • Verification instrumentation: A custom transducer checks output timing, simultaneous events, full/empty status, and head/tail updates.It checks that outputs occur 0.5 cycle after triggering.
  • Verification outcome: Verification found an error in simultaneous-event handling that could have gone unnoticed during simulation alone.The example is intended to illustrate the interaction of modeling, development, and verification.
  • Verification outcome: All states are explored across parameterized circular-buffer scenarios, ensuring functionality correctness for the tested configurations.Configurations vary buffer size, incoming packet types, injection rate, and ejection frequency.
  • Scalability: State-exploration execution time increases linearly with state-space size, while larger models encounter state explosion.Multiresolution modeling is identified as ongoing research addressing this problem.
  • Model scope: The exploration algorithm and DEVS-Suite extension support verification of coupled models, including a previously developed adaptive-router example.The paper reports creation and verification of coupled models.

6 NETWORK-ON-CHIP EXAMPLE MODELS

The Network-on-Chip examples demonstrate Constraint-DEVS and DEVS-Suite for modeling, simulation, and model checking, including routing, utilization, latency, and complex data exchange. Experiments show adaptive distribution improves processor-load balance but increases state-space size, while larger networks expose scalability limits.

  • NoC modeling: The NoC models represent packet generation, packetization, routing, crossbar allocation, and transmission through network links.The UPPAAL model uses independent processes, synchronization channels, and global variables for shared data.
  • Verification targets: The NoC experiments verify switch allocation, routing-related properties, processing-element utilization, and latency in models with more complex characteristics.Switch allocation correctness is identified as an important verification target, while performance-related properties are more difficult to verify in many environments.
  • DEVS-Suite modeling: Constraint-DEVS NoC models support both simulation and model checking, with multiple nodes and complex data exchange through Java objects.The same models can be simulated without modification, supporting validation alongside verification.
  • Experiment 1: PE utilization and task distribution: Adaptive task distribution produces a more balanced processor load than round-robin distribution, while adding explorable load-estimate variables.The adaptive distributor estimates processor load and creates a more balanced distribution across processing elements.
  • Experiment 2: scalability: 15-fold larger state spaces from adaptive distribution increase model-checking duration, and state-space growth makes whole-network exploration computationally impractical as nodes are added.The paper notes that networks larger than 16 nodes are impractical to check on basic computing platforms, motivating verification of components or network portions.
  • Framework capabilities: DEVS-Suite combines structural and behavioral modeling with selective state exploration, supporting verification and validation of complex systems despite execution-performance degradation at scale.The trade-off is that simulation and model-checking performance can rapidly degrade as model scale increases.

7 DISCUSSION

The discussion positions Constraint-DEVS and extended DEVS-Suite as general-purpose tools for modeling, validation, and verification. Their modular Parallel DEVS foundation, complex data-transfer support, and seamless simulation and model checking distinguish the framework, while comparisons are intentionally limited in scope.

  • Scope boundary: The comparison omits additional criteria because the research focus is limited to selected modeling, validation, and verification capabilities.The paper explicitly identifies this as a scope boundary for its comparison.
  • Contribution: Constraint-DEVS leverages DEVS modularity and component-based modeling to address scalability and complexity in system models.The discussion contrasts this approach with other DEVS-based tools and emphasizes Parallel DEVS modeling and simulation.
  • Integration: Parallel DEVS modeling and simulation in DEVS-Suite are seamless with Constraint-DEVS and model checking without side effects.This integration supports the framework's combined modeling, simulation, and verification role.
  • Comparison scope: The framework is compared with general modeling, validation, and verification formalisms rather than specialized NoC tools because the latter are domain-specific or lack comprehensive V&V support.The comparison focuses on the criteria relevant to this research.

8 CONCLUSION

The paper presents Constraint-DEVS and an extended DEVS-Suite framework that support both model simulation and model checking for bounded Parallel DEVS models. Network-on-Chip models demonstrate property verification, including state-based and path-based properties, while preserving simulation capabilities.

  • 8 CONCLUSION: The extended DEVS-Suite framework supports DEVS and Constraint-DEVS specifications with simulation and model checking, respectively.
  • 8 CONCLUSION: Network-on-Chip models were created with Constraint-DEVS and verified using the extended DEVS-Suite framework.The models demonstrate property expressions, property checking, data collection, and experimentation.
  • 8 CONCLUSION: DEVS-Suite verifies both path-based properties over prolonged system behavior and state-based properties evaluated at individual states.
  • 8 CONCLUSION: Constraint-DEVS removes the need to manually convert simulation models into less descriptive models for model checking.Parallel DEVS models are converted by placing prescribed bounds on state-variable values.
  • 8 CONCLUSION: The framework reuses DEVS-Suite’s simulation protocol and preserves its core architecture, modularity, modeling, and visualization capabilities.Switching between simulation and model checking is enabled through model configuration, while simulation capabilities remain intact.
  • 8 CONCLUSION: Future work targets flit-level Network-on-Chip models with virtual channels, flow control, and properties such as fairness and deadlock avoidance.

A VERIFICATION IN DEVS-SUITE FRAMEWORK

DEVS-Suite is extended to support Constraint-DEVS modeling and model-checking executions through a state exploration protocol. The extension adds Constraint-DEVS models and their executions while retaining the framework’s verification and validation orientation.

  • A VERIFICATION IN DEVS-SUITE FRAMEWORK: DEVS-Suite’s verification extension has two parts: developing Constraint-DEVS models and executing them with the state exploration protocol.
  • A VERIFICATION IN DEVS-SUITE FRAMEWORK: The VerifiableAtomic class provides the framework-level basis for verification and validation.

A.1 Constraint-DEVS

Constraint-DEVS augments DEVS-Suite models with bounded state variables, bounded ports, and verification-specific atomic-model functionality. These structures support state-space exploration while retaining simulation-mode operation.

  • A.1 Constraint-DEVS: VerifiableAtomic extends ViewableAtomic with initial states, invalid states, state-transition checking, initialization, and mode switching.The setToVerificationMode operation switches between simulation and model-checking modes.
  • A.1 Constraint-DEVS: Constraint-DEVS state variables can be bounded using regular expressions and incorporated into model execution.The original DEVS-Suite framework lacks support for bounded state variables, motivating the extensions.
  • A.1 Constraint-DEVS: Constraint-DEVS adds base classes that support bounded state variables and bounded incoming-port values for state-space exploration.StateVar requires bounded, iterable state variables, while PortState bounds port content values and supports possible external events.
  • A.1 Constraint-DEVS: Messages communicate content objects through ports, and PortState bounds the values of those content objects.
  • A.1 Constraint-DEVS: The State class aggregates state variables, ports and their possible values, and visited and unvisited state data structures.A model can contain multiple StateVar and PortState instances but only one State instance.
  • A.1 Constraint-DEVS: The UML diagrams provide partial views of the classes and omit complete attributes, methods, and initializations; fuller diagrams appear in Section A.2.

A.2 State Space Exploration Protocol

The Constraint-DEVS state exploration protocol systematically explores reachable states by injecting possible bounded inputs, executing the model through the simulation engine, and tracking visited and unvisited states. DEVS-Suite’s verification engine coordinates this process while reusing the simulation architecture and visualization capabilities.

  • A.2 State Space Exploration Protocol: The VerificationEngine manages state exploration, instantiates input generators and transducers, and tracks visited and unvisited states.
  • A.2 State Space Exploration Protocol: The protocol uses a generator, transducer, target model, and visited and unvisited state sets to perform reachability analysis.The generator injects possible input combinations, while the transducer collects state-transition traces and checking results.
  • A.2 State Space Exploration Protocol: State exploration proceeds through initialization, a main loop over new states, input injection, housekeeping, and termination.The process begins with initial and unsafe states, applies all possible inputs, stores resulting states, and terminates when no unvisited states remain.
  • A.2 State Space Exploration Protocol: For each current state, the simulation engine executes the model for one cycle after a possible input combination is applied.
  • A.2 State Space Exploration Protocol: Housekeeping stores resulting states, adds unvisited states to Q, and moves fully explored current states into V.When Q is empty, the transducer provides the trace and property-checking results.
  • A.2 State Space Exploration Protocol: The framework’s UML extensions support both simulation and model checking while preserving the existing simulation architecture and modularity.VerificationEngine operates above reused simulation classes, and the class relationships support both execution modes.
  • A.2 State Space Exploration Protocol: VerifiableAtomic and VerifiableDigraph extend viewable classes, enabling reuse of animation, trajectory generation, and simulation without changing Constraint-DEVS models.
  • A.2 State Space Exploration Protocol: DEVS-Suite switches between verifying and simulating during Running mode, with initialization selecting the execution mode.Reset returns the system to Initialization, while suspend and continue control pausing and resuming.
Loading 2608.22095v1…