Visual counterexample explanation for model checking with OERITTE

Polina Ovsiannikova, Igor Buzhinsky, Antti Pakonen, Valeriy Vyatkin

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

1 Sitaatiot (Scopus)

Abstrakti

Despite being one of the most reliable approaches for ensuring system correctness, model checking requires auxiliary tools to fully avail. In this work, we tackle the issue of its results being hard to interpret and present OERITTE, a tool for automatic visual counterexample explanation for function block diagrams. To learn what went wrong, the user can inspect a parse tree of the violated LTL formula and a table view of a counterexample, where important variables are highlighted. Then, on the function block diagram of the system under verification, they can receive a visualization of causality relationships between the calculated values of interest and intermediate results or inputs of the function block diagram. Thus, OERITTE serves to decrease formal model and specification debugging efforts along with making model checking more utilizable for complex industrial systems.

AlkuperäiskieliEnglanti
OtsikkoProceedings of 2020 25th International Conference on Engineering of Complex Computer Systems, ICECCS 2020
ToimittajatYi Li, Alan Liew
KustantajaIEEE
Sivut1-10
Sivumäärä10
ISBN (elektroninen)9781728185583
DOI - pysyväislinkit
TilaJulkaistu - 19 maaliskuuta 2021
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Engineering of Complex Computer Systems - Singapore, Singapore
Kesto: 4 maaliskuuta 20216 maaliskuuta 2021
Konferenssinumero: 25

Conference

ConferenceInternational Conference on Engineering of Complex Computer Systems
LyhennettäICECCS
MaaSingapore
KaupunkiSingapore
Ajanjakso04/03/202106/03/2021

Sormenjälki Sukella tutkimusaiheisiin 'Visual counterexample explanation for model checking with OERITTE'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Siteeraa tätä