Verificação de deadlock e não-determinismo em ações de SysML 2.0

Abstract

The growing complexity of systems has led to an increasing effort to validate them. Focusing on initiatives for creating tools to identify problems as early as possible has been a very desirable approach to minimize costs and efforts. Some problems like deadlock and nondeterminism can become increasingly difficult to detect due to the concurrent and distributed nature that systems can present. The SysML 2.0 language has been developed by OMG. It provides notation for actions that can be used to model behaviors, even concurrent ones, which makes them suitable for describing the dynamics of these systems. Several works propose formal semantics to SysML 1.0 models for verification purposes, including deadlock verification. But our proposal is distinct in that we provide a formal semantics for SysML 2.0 actions that not only check for the presence of deadlocks, but also nondeterminism. The latter is generally neglected in the literature, although it can be considered relevant in complex system architectures. This entire verification process is automated and also provides full traceability back to SysML 2.0 in case a problem is detected in the model. Therefore, the user does not need to understand or manipulate formal notations in any part of the process. Therefore, our main contribution is a checker for analyzing properties of SysML 2.0 actions, specifically deadlock and nondeterminism, not requiring any knowledge on the underlying formal semantics.