Nicolas Markey

Abstract

Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results.

@inproceedings{formats2020-JMMNS,
  author =              {J{\'e}ron, Thierry and Markey, Nicolas and
                         Mentr{\'e}, David and Noguchi, Reiya and Sankur,
                         Ocan},
  title =               {Incremental methods for checking real-time
                         consistency},
  editor =              {Bertrand, Nathalie and Jansen, Nils},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'20)},
  acronym =             {{FORMATS}'20},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {12288},
  pages =               {249-264},
  year =                {2020},
  month =               sep,
  doi =                 {10.1007/978-3-030-57628-8_15},
  abstract =            {Requirements engineering is a key phase in the
                         development process. Ensuring that requirements are
                         consistent is essential so that they do not conflict
                         and admit implementations. We~consider the formal
                         verification of rt-consistency, which imposes that
                         the inevitability of definitive errors of a
                         requirement should be anticipated, and that of
                         partial consistency, which was recently introduced
                         as a more effective check. We~generalize and
                         formalize both notions for discrete-time timed
                         automata, develop three incremental algorithms, and
                         present experimental results.},
}