sxm 0.0.1

A Stream X-Machine library for formal modeling, visualization, and model-based testing.
Documentation
  • Coverage
  • 34.57%
    28 out of 81 items documented0 out of 32 items with examples
  • Size
  • Source code size: 60.38 kB This is the summed size of all the files inside the crates.io package for this release.
  • Documentation size: 2.41 MB This is the summed size of all files generated by rustdoc for all configured targets
  • Links
  • Ruben1729/sxm
    0 0 0
  • crates.io
  • Dependencies
    • —
  • Versions
  • Owners
  • Ruben1729

Stream X-Machines in Rust

Introduction

sxm is a Rust framework for modeling, visualizing, and testing systems using Stream X-Machines (SXM) and Communicating Stream X-Machine Systems (CSXMS).

Unlike traditional Finite State Machines (FSMs) that only model control flow, Stream X-Machines integrate dynamic data structures (memory) with the state transition logic. This library provides a type-safe, trait-based approach to implementing these formal models in embedded systems and high-reliability software.

Features

  • Formal Specification: Define machines with typed Inputs ($\Sigma$), Outputs ($\Gamma$), States ($Q$), Memory ($M$), and Processing Functions ($\Phi$).
  • Model-Based Testing (MBT): automatically generate test suites to verify your implementation against the model.
    • Logic Verification: Implements the W-Method to generate conformance tests that prove the control logic is correct.
    • Robustness Testing: Generates Input-Completeness tests to ensure the system handles invalid or unexpected inputs gracefully without crashing.
    • Symbolic Execution: Uses memory-aware Breadth-First Search to discover data-dependent transitions (e.g., cracking a PIN code to test a locked state).
  • System Visualization:
    • Generate Graphviz (DOT) diagrams of the internal state machine logic (the associated finite automaton).
    • Generate System Context diagrams for black-box integration views.
    • Visualize connected CSXM systems with routing logic (Matrix $E$).
  • Communicating Systems: Support for connecting multiple SXMs (e.g., a Keypad and a Door) via adapter patterns to model complex, distributed behaviors.

Reference

This library is an implementation of the formal verification and testing concepts presented in:

Testing Communicating Stream X-machines F. Ipate, T. Bălănescu, and G. Eleftherakis Department of Computer Science and Mathematics, University of Pitesti, Romania & CITY College, Greece.

Specifically, it implements the testing conditions and methodologies described for deterministic stream X-machines and addresses the "Design for Test" conditions such as Input-Completeness and Output-Distinguishability.

License

Licensed under either of

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.