[en] Trace checking is a verification technique widely used in Cyber-physical system (CPS) development, to verify whether execution traces satisfy or violate properties expressing system requirements. Often these properties characterize complex signal behaviors and are defined using domain-specific languages, such as SB-TemPsy-DSL, a pattern-based specification language for signal-based temporal properties. Most of the trace-checking tools only yield a Boolean verdict. However, when a property is violated by a trace, engineers usually inspect the trace to understand the cause of the violation; such manual diagnostic is time-consuming and error-prone. Existing approaches that complement trace-checking tools with diagnostic capabilities either produce low-level explanations that are hardly comprehensible by engineers or do not support complex signal-based temporal properties.
In this paper, we propose TD-SB-TemPsy, a trace-diagnostic approach for properties expressed using SB-TemPsy-DSL. Given a property and a trace that violates the property, TD-SB-TemPsy determines the root cause of the property violation. TD-SB-TemPsy relies on the concepts of violation cause, which characterizes one of the behaviors of the system that may lead to a property violation, and diagnoses, which are associated with violation causes and provide additional information to help engineers understand the violation cause. As part of TD-SB-TemPsy, we propose a language-agnostic methodology to define violation causes and diagnoses. In our context, its application resulted in a catalog of 34 violation causes, each associated with one diagnosis, tailored to properties expressed in SB-TemPsy-DSL.
We assessed the applicability of TD-SB-TemPsy on two datasets, including one based on a complex industrial case study. The results show that TD-SB-TemPsy could finish within a timeout of 1 min for ≈ 83.66% of the trace-property combinations in the industrial dataset, yielding a diagnosis in ≈ 99.84% of these cases; moreover, it also yielded a diagnosis for all the trace-property combinations in the other dataset. These results suggest that our tool is applicable and efficient in most cases.
Research center :
Interdisciplinary Centre for Security, Reliability and Trust (SnT) > SVV - Software Verification and Validation
Disciplines :
Computer science
Author, co-author :
Boufaied, Chaima; University of Ottawa
Menghi, Claudio
Bianculli, Domenico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
Briand, Lionel ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > SVV
External co-authors :
yes
Language :
English
Title :
Trace Diagnostics for Signal-based Temporal Properties
Publication date :
May 2023
Journal title :
IEEE Transactions on Software Engineering
ISSN :
1939-3520
Publisher :
Institute of Electrical and Electronics Engineers, New-York, United States - New York
Volume :
49
Issue :
5
Pages :
3131-3154
Peer reviewed :
Peer Reviewed verified by ORBi
Focus Area :
Security, Reliability and Trust
European Projects :
H2020 - 957254 - COSMOS - DevOps for Complex Cyber-physical Systems
C. Boufaied, C. Menghi, D. Bianculli, L. Briand, and Y. Isasi Parache, "Trace-checking signal-based temporal properties: A model-driven approach," in Proc. IEEE/ACMInt. Conf. Automated Softw. Eng., NewYork, NY, USA, 2020, pp. 1004-1015.
C. Menghi, E. Viganò, D. Bianculli, and L. C. Briand, "Trace-checking CPS properties: Bridging the cyber-physical gap," in Proc. IEEE Int. Conf. Softw. Eng., Los Alamitos, CA, USA, 2021, pp. 847-859.
C. Menghi, S.Nejati, K. Gaaloul, and L. C. Briand, "Generating automated and online test oracles for simulink models with continuous and uncertain behaviors," in Proc. ACMEur. Softw. Eng. Conf. Symp. Found. Softw. Eng., New York, NY, USA, 2019, pp. 27-38.
F. Gorostiaga and C. Sánchez, "Striver: Stream runtime verification for real-time event-streams," in Proc. Int. Conf. Runtime Verification, Cham: Springer, 2018, pp. 282-298.
L. Convent, S. Hungerecker, M. Leucker, T. Scheffel, M. Schmitz, and D. Thoma, "TeSSLa: Temporal stream-based specification language," in Proc. Braz. Symp. Formal Methods, Cham: Springer, 2018, pp. 144-162.
P. Faymonville, B. Finkbeiner, S. Schirmer, and H. Torfah, "A streambased specification language for network monitoring," in Proc. Int. Conf. Runtime Verification, 2016, pp. 152-168. [Online]. Available: https://10. 1007/978-3-319-46982-9_10
C. Menghi, C. Tsigkanos, P. Pelliccione, C. Ghezzi, and T. Berger, "Specification patterns for robotic missions," IEEE Trans. Softw. Eng., vol. 47, no. 10, pp. 2208-2224, Oct. 2021.
M. Fowler, Domain-Specific Languages. Boston, MA, USA: Pearson Education, 2010.
C. Boufaied, M. Jukss, D. Bianculli, L. C. Briand, and Y. Isasi Parache, "Signal-based properties of cyber-physical systems: Taxonomy and logic-based characterization," J. Syst. Softw., vol. 174, 2021, Art. no. 110881. [Online]. Available: https://www.sciencedirect.com/ science/article/pii/S0164121220302715
T. Ferrère, O. Maler, and D. Niĉković, "Trace diagnostics using temporal implicants," in Proc. Int. Symp. Automated Technol. Verification Anal., Cham: Springer, 2015, pp. 241-258.
S. Mukherjee and P. Dasgupta, "Computing minimal debugging windows in failure traces of AMS assertions," IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst., vol. 31, no. 11, pp. 1776-1781, Nov. 2012.
I. Beer, S. Ben-David, H. Chockler, A. Orni, and R. Trefler, "Explaining counterexamples using causality," in Proc. Int. Conf. Comput. Aided Verification, Berlin, Heidelberg: Springer, 2009, pp. 94-108.
D. Niĉković, O. Lebeltel, O. Maler, T. Ferrère, and D. Ulus, "AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic," in Proc. Int.Conf. ToolsAlgorithms ConstructionAnal. Syst.,Cham: Springer, 2018, pp. 303-319.
J. H. Dawes and G. Reger, "Explaining violations of properties in controlflow temporal logic," in Proc. Int. Conf. Runtime Verification, Cham: Springer, 2019, pp. 202-220.
W. Dou, D. Bianculli, and L. Briand, "Model-driven trace diagnostics for pattern-based temporal specifications," in Proc. IEEE/ACM21th Int. Conf. Model Driven Eng. Lang. Syst., New York, NY, USA, 2018, pp. 278-288.
Q. Luo et al., "RV-monitor: Efficient parametric runtime verification with simultaneous properties," in Proc. Int. Conf. Runtime Verification, Cham: Springer, 2014, pp. 285-300. [Online].Available: https://doi.org/10.1007/ 978-3-319-11164-3_24
W. Dou, D. Bianculli, and L. Briand, "A model-driven approach to trace checking of pattern-based temporal properties," in Proc. IEEE/ACM 20th Int. Conf. Model Driven Eng. Lang. Syst., Los Alamitos, CA, USA, 2017, pp. 323-333.
D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann, "Generation of formal requirements from structured natural language," in Proc. Int. Work. Conf. Requirements Eng.: Found. Softw. Qual., Cham: Springer International Publishing, 2020, pp. 19-35.
G. Ernst et al., "Arch-comp 2021 category report: Falsification with validation of results," in Proc. 8th Int.Workshop Appl. Verification Continuous Hybrid Syst., 2021, pp. 133-152.
Wikipedia contributors, "Beta angle-Wikipedia, the free encyclopedia," 2021. Accessed: Sep. 02, 2021. [Online]. Available: https://en.wikipedia. org/w/index.php?title=Beta_angle&oldid=1035086598
T. Ott, A. Benoit, P.Van den Braembussche, and W. Fichter, "ESA pointing error engineering handbook," in Proc. 8th Int. ESAConf.Guid.,Navigation Control Syst., Bruxelles: European Space Agency, 2011, pp. 1-12.
A. J. Robinson and A. Voronkov, Handbook of Automated Reasoning. vol. 1. Amsterdam, The Netherlands: Elsevier, 2001.
L. De Moura and N. Bjørner, "Z3: An efficient SMT solver," in Proc. Theory Pract. Softw., 14th Int. Conf. Tools Algorithms Construction Anal. Syst., Berlin, Heidelberg: Springer-Verlag, 2008, pp. 337-340.
D. Giannakopoulou, T. Pressburger, A. Mavridou, and J. Schumann, "Automated formalization of structured natural language requirements," Inf. Softw. Technol., vol. 137, 2021, Art. no. 106590.
E. Bartocci et al., "First international competition on runtime verification: Rules, benchmarks, tools, and final results of CRV 2014," Int. J. Softw. Tools Technol. Tran., vol. 21, no. 1, pp. 31-70, 2019. [Online]. Available: https://doi.org/10.1007/s10009-017-0454-5
G. Reger, "A report of RV-cubes 2017," in Proc. Int. Workshop Competitions, Usability, Benchmarks, Eval., Standardisation Runtime Verification Tools, Seattle, WA, USA, 2017, pp. 1-9. [Online]. Available: https://doi.org/10.29007/2496
S. Krstić and J. Schneider, "A benchmark generator for online first-order monitoring," in Proc. Int. Conf. Runtime Verification, Springer, 2020, pp. 482-494.
J. Li and K. Y. Rozier, "Mltl benchmark generation via formula progression," in Proc. Int. Conf. Runtime Verification, Springer, 2018, pp. 426-433.
D. Ulus, "Timescales: A benchmark generator for mtl monitoring tools," in Proc. Int. Conf. Runtime Verification, Springer, 2019, pp. 402-412.
C. Menghi, E. Viganò, D. Bianculli, and L. C. Briand, "Trace-checking CPS properties: Bridging the cyber-physical gap," in Proc. IEEE/ACM 43rd Int. Conf. Softw. Eng., 2021, pp. 847-859.
X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. Butts, "Powertrain control verification benchmark," in Proc. ACM 17th Int. Conf. Hybrid Syst.: Comput.Control,NewYork,NY, USA, 2014, pp. 253-262. [Online]. Available: https://doi.org/10.1145/2562059.2562140
J. Szabados and P. Vértesi, Interpolation of Functions. Singapore: World Scientific, 1990.
C. Menghi, S. Nejati, L. C. Briand, and P. Yago Isasi, "Approximationrefinement testing of compute-intensive cyber-physical models: An approach based on system identification," in Proc. IEEE/ACM42nd Int. Conf. Softw. Eng., New York, NY, USA, 2020.
Y. Annpureddy,C.Liu,G. Fainekos, and S. Sankaranarayanan, "S-TaLiRo: A tool for temporal logic falsification for hybrid systems," in Proc. Int. Conf. Tools Algorithms Construction Anal. Syst., Berlin, Heidelberg: Springer, 2011, pp. 254-257.
D. Niĉković and T. Yamaguchi, "RTAMT: Online robustness monitors from STL," in Proc. Int. Symp. Automated Technol. Verification Anal., Springer, 2020, pp. 564-571.
C. Boufaied, "TD-SB-TemPsy supplementary material," 2023. [Online]. Available: https://figshare.com/articles/software/TD-SB-TemPsy_ SupplementaryMaterial/21956924
C. Boufaied, C. Menghi, D. Bianculli, and L. Briand, "TD-SB-TemPsy software artifact," 2023. [Online].Available: https://figshare.com/articles/ software/TD-SB-TemPsy/21954563
C. Menghi, A. M. Rizzi, and A. Bernasconi, "Integrating topological proofs with model checking to instrument iterative design," in Proc. Int. Conf. Fundam. Approaches Softw. Eng., Cham: Springer, 2020, pp. 53-74.
V. Schuppan, "Towards a notion of unsatisfiable and unrealizable cores for LTL," Sci. Comput. Program., vol. 77, no. 7/8, pp. 908-939, 2012.
F. Hantry and M.-S. Hacid, "Handling conflicts in depth-first search for LTL tableau to debug compliance based languages," Electron. Proc. Theor. Comput. Sci., vol. 68, 2011, pp. 39-53.
G. Zheng et al., "Flack: Counterexample-guided fault localization for alloy models," in Proc. IEEE Int. Conf. Softw. Eng., Los Alamitos, CA, USA, 2021, pp. 637-648.
M. Chechik and A. Gurfinkel, "A framework for counterexample generation and exploration," in Proc. Int. Conf. Fundam. Approaches Softw. Eng., Berlin, Heidelberg: Springer, 2005, pp. 220-236.
T. Bochot, P. Virelizier, H. Waeselynck, and V. Wiels, "Paths to property violation: A structural approach for analyzing counter-examples," in Proc. IEEE Int. Symp.High Assurance Syst. Eng., Los Alamitos, CA, USA, 2010, pp. 74-83.
A. Griggio, M. Roveri, and S. Tonetta, "Certifying proofs for LTL model checking," in Proc. IEEE Formal Methods Comput. Aided Des., Los Alamitos, CA, USA, 2018, pp. 1-9.
F. Funke, S. Jantsch, and C. Baier, "Farkas certificates and minimal witnesses for probabilistic reachability constraints," in Proc. Int. Conf. Tools Algorithms Construction Anal. Syst., Cham: Springer, 2020, pp. 324-345.
N. Timm, S. Gruner, M. Nxumalo, and J. Botha, "Model checking safety and liveness via k-induction and witness refinement with constraint generation," Sci. Comput. Program., vol. 200, 2020, Art. no. 102532.
A. Gurfinkel and M. Chechik, "Proof-like counter-examples," in Proc. Int. Conf. Tools Algorithms Construction Anal. Syst., Berlin, Heidelberg: Springer, 2003, pp. 160-175.
D. Peled and L. Zuck, "Frommodel checking to a temporal proof," in Proc. Int. SPIN Workshop Model Checking Softw., Berlin Heidelberg: Springer-Verlag, 2001, pp. 1-14.
A. Bernasconi, C.Menghi, P. Spoletini, L. D. Zuck, and C. Ghezzi, "From model checking to a temporal proof for partial models," in Proc. Int. Conf. Softw. Eng. Formal Methods, Cham: Springer, 2017, pp. 54-69.
D. Peled, A. Pnueli, and L. Zuck, "From falsification to verification," in Proc. Int. Conf. Found. Softw. Technol. Theor. Comput. Sci., Berlin, Heidelberg: Springer, 2001, pp. 292-304.
A. Mebsout and C. Tinelli, "Proof certificates for SMT-based model checkers for infinite-state systems," in Proc. IEEE Formal Methods Comput.-Aided Des., Los Alamitos, CA, USA, 2016, pp. 117-124.
D. Basin, B. N. Bhatt, and D. Traytel, "Optimal proofs for linear temporal logic on lasso words," in Proc. Int. Symp. Automated Technol. Verification Anal., Cham: Springer, 2018, pp. 37-55.
A. Pnueli and Y. Kesten, "A deductive proof system for CTL," in Proc. Int. Conf.Concurrency Theory,Berlin,Heidelberg: Springer-Verlag, 2002, pp. 24-40.
I. Balaban, A. Pnueli, and L. D. Zuck, "Proving the refuted: Symbolic model checkers as proof generators," in Concurrency, Compositionality, and Correctness. Berlin, Heidelberg: Springer, 2010, pp. 221-236.
S. Grebing and M. Ulbrich, "Usability recommendations for user guidance in deductive program verification," in Deductive Software Verification: FuturePerspectives:Reflections on theOccasion of 20 Years ofKeY,Cham, Switzerland: Springer, 2020, pp. 261-284. [Online].Available: https://doi. org/10.1007/978-3-030-64354-6_11