TY - GEN
T1 - Two Decades of Industrializing Formal Verification
T2 - 30th International Symposium on Model Checking Software, SPIN 2024
AU - Cleaveland, Rance
AU - Hansel, David
AU - Sims, Steve
AU - A. Smolka, Scott
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.
PY - 2025
Y1 - 2025
N2 - Reactis® is a suite of tools produced by Reactive Systems, Inc. (RSI), for automated test generation from, and verification of, systems given in either the modeling languages MATLAB® / Simulink® / Stateflow® of The MathWorks, Inc., or ANSI C. RSI was founded by three of the authors of this paper in 1999, with the first release of Reactis coming in 2002; the tools are used in the testing and validation of embedded control systems in a variety of industries, including automotive and aerospace / defense. This paper traces the development of the Reactis tool suite from earlier research on model-checking tools undertaken by the authors and others, highlighting the importance of both the foundational basis of Reactis and the essential adaptations and extensions needed for a commercially successful product.
AB - Reactis® is a suite of tools produced by Reactive Systems, Inc. (RSI), for automated test generation from, and verification of, systems given in either the modeling languages MATLAB® / Simulink® / Stateflow® of The MathWorks, Inc., or ANSI C. RSI was founded by three of the authors of this paper in 1999, with the first release of Reactis coming in 2002; the tools are used in the testing and validation of embedded control systems in a variety of industries, including automotive and aerospace / defense. This paper traces the development of the Reactis tool suite from earlier research on model-checking tools undertaken by the authors and others, highlighting the importance of both the foundational basis of Reactis and the essential adaptations and extensions needed for a commercially successful product.
KW - Guided simulation
KW - Instrumentation-based specification and verification
KW - MATLAB / Simulink / Stateflow
KW - Model-based testing
KW - Reactis
UR - https://www.scopus.com/pages/publications/85207653713
U2 - 10.1007/978-3-031-66149-5_5
DO - 10.1007/978-3-031-66149-5_5
M3 - Conference contribution
AN - SCOPUS:85207653713
SN - 9783031661488
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 87
EP - 105
BT - Model Checking Software - 30th International Symposium, SPIN 2024, Proceedings
A2 - Neele, Thomas
A2 - Wijs, Anton
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 8 April 2024 through 9 April 2024
ER -