Nicolas Markey

Abstract

Partial observability and controllability are two well-known issues in test-case synthesis for reactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. We extend a previous approach to this problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that try to minimize both cooperations of the system and distance to the satisfaction of a test purpose or to the next cooperation, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method. We finally propose a symbolic algorithm to compute those strategies.

@article{fmsd60(2)-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Control strategies for off-line testing of timed
                         systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {60},
  number =              {2},
  pages =               {147-194},
  year =                {2022},
  month =               apr,
  doi =                 {10.1007/s10703-022-00403-w},
  abstract =            {Partial observability and controllability are two
                         well-known issues in test-case synthesis for
                         reactive systems. We address the problem of partial
                         control in the synthesis of test cases from
                         timed-automata specifications. We extend a previous
                         approach to this problem from the untimed to the
                         timed setting. This extension requires a deep
                         reworking of the models, game interpretation and
                         test-synthesis algorithms. We exhibit strategies of
                         a game that try to minimize both cooperations of the
                         system and distance to the satisfaction of a test
                         purpose or to the next cooperation, and prove they
                         are winning under some fairness assumptions. This
                         entails that when turning those strategies into test
                         cases, we get properties such as soundness and
                         exhaustiveness of the test synthesis method. We
                         finally propose a symbolic algorithm to compute
                         those strategies.},
}