This paper presents an automated and scalable matrix-based verification framework for classical soundness in Robustness Diagrams with Loop and Time Controls (RDLT), leveraging a property known as L-safeness. Classical soundness of theoretical and real-world systems is an important property as it implies that such systems observe proper termination and the absence of deadlocks in their components and processes. While existing methods focus solely on relaxed soundness, a weakened form of classical soundness, this paper introduces a comprehensive L-safeness verification system. This verification system consists of two main components. First, it includes a transformation that converts an RDLT into a set of matrix representations. Second, it features an automated validation process that uses matrix operations to verify fundamental L-safeness conditions, i.e. ensuring that allowances and restrictions to resource utility of the RDLT components, as well as their split-join structures, form a model design that enforces the requirements of classical soundness. The framework’s central theoretical contribution is the established equivalence: an RDLT is classical sound if and only if it is L-safe. This allows L-safeness to serve as a computationally tractable proxy for verifying classical soundness. In support, we provide the proofs of correctness of our verification system and its time and space complexity. Finally, we report our results for functional testing to demonstrate the completeness and correctness of our automation tool for the verification of L-safeness.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Automated Verification of Classical Soundness in Robustness Diagrams with Loop and Time Controls via L-safeness

  • Andrei Luz B. Asoy,
  • Jasmine A. Malinao

摘要

This paper presents an automated and scalable matrix-based verification framework for classical soundness in Robustness Diagrams with Loop and Time Controls (RDLT), leveraging a property known as L-safeness. Classical soundness of theoretical and real-world systems is an important property as it implies that such systems observe proper termination and the absence of deadlocks in their components and processes. While existing methods focus solely on relaxed soundness, a weakened form of classical soundness, this paper introduces a comprehensive L-safeness verification system. This verification system consists of two main components. First, it includes a transformation that converts an RDLT into a set of matrix representations. Second, it features an automated validation process that uses matrix operations to verify fundamental L-safeness conditions, i.e. ensuring that allowances and restrictions to resource utility of the RDLT components, as well as their split-join structures, form a model design that enforces the requirements of classical soundness. The framework’s central theoretical contribution is the established equivalence: an RDLT is classical sound if and only if it is L-safe. This allows L-safeness to serve as a computationally tractable proxy for verifying classical soundness. In support, we provide the proofs of correctness of our verification system and its time and space complexity. Finally, we report our results for functional testing to demonstrate the completeness and correctness of our automation tool for the verification of L-safeness.