Nicolas Markey

Résumé

We consider the problem of repairing inconsistent real-time requirements with respect to two consistency notions: non-vacuity, which means that each requirement can be realized without violating other ones, and rt-consistency, which means that inevitable violations are detected immediately. We provide an iterative algorithm, based on solving SMT queries, to replace designated parameters of real-time requirements with new Boolean expressions and time constraints, so that the resulting set of requirements becomes consistent.

@inproceedings{atva2022-NSJMM,
  author =              {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron,
                         Thierry and Markey, Nicolas and Mentr{\'e}, David},
  title =               {Repairing Real-Time Requirements},
  editor =              {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and
                         Wu, Zhilin},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'22)},
  acronym =             {{ATVA}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13505},
  pages =               {371-387},
  year =                {2022},
  month =               oct,
  doi =                 {10.1007/978-3-031-19992-9_24},
  abstract =            {We~consider the problem of repairing inconsistent
                         real-time requirements with respect to two
                         consistency notions: non-vacuity, which means that
                         each requirement can be realized without violating
                         other ones, and rt-consistency, which means that
                         inevitable violations are detected immediately.
                         We~provide an iterative algorithm, based on solving
                         SMT queries, to replace designated parameters of
                         real-time requirements with new Boolean expressions
                         and time constraints, so that the resulting set of
                         requirements becomes consistent.},
}