Quantitative reactive modeling and verification
Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer Science Research and Development. 28(4), 331–344.
Download
Journal Article
| Published
| English
Scopus indexed
Author
Department
Abstract
Formal verification aims to improve the quality of software by detecting errors before they do harm. At the basis of formal verification is the logical notion of correctness, which purports to capture whether or not a program behaves as desired. We suggest that the boolean partition of software into correct and incorrect programs falls short of the practical need to assess the behavior of software in a more nuanced fashion against multiple criteria. We therefore propose to introduce quantitative fitness measures for programs, specifically for measuring the function, performance, and robustness of reactive programs such as concurrent processes. This article describes the goals of the ERC Advanced Investigator Project QUAREM. The project aims to build and evaluate a theory of quantitative fitness measures for reactive models. Such a theory must strive to obtain quantitative generalizations of the paradigms that have been success stories in qualitative reactive modeling, such as compositionality, property-preserving abstraction and abstraction refinement, model checking, and synthesis. The theory will be evaluated not only in the context of software and hardware engineering, but also in the context of systems biology. In particular, we will use the quantitative reactive models and fitness measures developed in this project for testing hypotheses about the mechanisms behind data from biological experiments.
Publishing Year
Date Published
2013-10-05
Journal Title
Computer Science Research and Development
Publisher
Springer
Volume
28
Issue
4
Page
331 - 344
IST-REx-ID
Cite this
Henzinger TA. Quantitative reactive modeling and verification. Computer Science Research and Development. 2013;28(4):331-344. doi:10.1007/s00450-013-0251-7
Henzinger, T. A. (2013). Quantitative reactive modeling and verification. Computer Science Research and Development. Springer. https://doi.org/10.1007/s00450-013-0251-7
Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” Computer Science Research and Development. Springer, 2013. https://doi.org/10.1007/s00450-013-0251-7.
T. A. Henzinger, “Quantitative reactive modeling and verification,” Computer Science Research and Development, vol. 28, no. 4. Springer, pp. 331–344, 2013.
Henzinger TA. 2013. Quantitative reactive modeling and verification. Computer Science Research and Development. 28(4), 331–344.
Henzinger, Thomas A. “Quantitative Reactive Modeling and Verification.” Computer Science Research and Development, vol. 28, no. 4, Springer, 2013, pp. 331–44, doi:10.1007/s00450-013-0251-7.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
IST-2016-626-v1+1_s00450-013-0251-7.pdf
570.36 KB
Access Level
Open Access
Date Uploaded
2018-12-12
MD5 Checksum
f117a00f9f046165bfa95595681e08a0