Formal methods are increasingly used in the development of safety-critical systems, offering a rigorous approach from model to implementation. However, in the validation process, the nondeterminism is a hindrance in their application, as it can lead to flaky tests or flaky scenarios. Scenarios written for models that implement nondeterminism produce unpredictable outcomes by complicating model validation and reducing developer confidence. In this paper, we present an approach to address the nondeterminism in the validation phase when using the Asmeta framework. We extend the Avalla language, used for scenario specification in Asmeta, to allow deterministic control over nondeterministic choices. This extension ensures that scenarios written for nondeterministic models execute predictably by eliminating flakiness. We demonstrate our approach using a running example of an automatic coffee vending machine.

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

Eliminating Flakiness: Deterministic Control for Validating Nondeterministic Asmeta Specifications

  • Andrea Bombarda,
  • Silvia Bonfanti,
  • Angelo Gargantini,
  • Nico Pellegrinelli

摘要

Formal methods are increasingly used in the development of safety-critical systems, offering a rigorous approach from model to implementation. However, in the validation process, the nondeterminism is a hindrance in their application, as it can lead to flaky tests or flaky scenarios. Scenarios written for models that implement nondeterminism produce unpredictable outcomes by complicating model validation and reducing developer confidence. In this paper, we present an approach to address the nondeterminism in the validation phase when using the Asmeta framework. We extend the Avalla language, used for scenario specification in Asmeta, to allow deterministic control over nondeterministic choices. This extension ensures that scenarios written for nondeterministic models execute predictably by eliminating flakiness. We demonstrate our approach using a running example of an automatic coffee vending machine.