Izvorni znanstveni članak
https://doi.org/10.24138/jcomss-2025-0028
Formal Verification of the Correctness and Soundness of a Pomset-to-LTS Transformation Algorithm
Asma Bezza
; University of Oum El Bouaghi 04000, Algeria
*
Rohallah Benaboud
; University of Oum El Bouaghi 04000, Algeria
Toufik-Messaoud Maarouk
; University Abbes Laghrour Khenchela, Algeria
Rabea Ameur-Boulifa
; Institut Polytechnique de Paris, France
* Dopisni autor.
Sažetak
In this paper, we present a comprehensive proof of the correctness and soundness of our previously published algorithm for transforming partially ordered multisets (Pomsets) into labeled transition systems (LTS). Our approach rigorously ensures that the transformation algorithm preserves the behavioral semantics of the original Pomset, ensuring that the resulting LTS accurately represents the concurrent and sequential dependencies inherent in the Pomset. We employ Hoare logic to formally verify the correctness of the algorithm, proving that every valid Pomset is transformed into a corresponding LTS without loss of information. Additionally, we provide detailed proofs of soundness, showing that the algorithm produces an LTS if and only if the input is a valid Pomset. This algorithm was initially proposed as part of our new refinement proof approach, which has already been published. However, the correctness of the algorithm had not been formally proven until now. These results confirm the reliability and robustness of our transformation algorithm, making it a valuable tool for modeling and analyzing concurrent systems.
Ključne riječi
Formal verification; Correctness; soundness; Pomset; LTS; Hoare-logic
Hrčak ID:
336752
URI
Datum izdavanja:
20.10.2025.
Posjeta: 308 *