Quantitative Models and Analysis for Reactive Systems

Claus Thrane

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

Resumé

The majority of modern software and hardware systems are reactive systems, where input provided by the user (possibly another system) and the output of the system is exchanged continuously throughout the (possibly) indefinite execution of the system. Natural examples include control systems, mobile phones and websites.
Acknowledging that now more than ever, systems come in contact with the physical world, we need to revise the way we construct models and verification algorithms, to take into account the behavior of systems in the presence of approximate, or quantitative information, provided by the environment in which they are embedded.
This thesis studies the semantics and properties of a model-based framework for re- active systems, in which models and specifications are assumed to contain quantifiable information, such as references to time or energy. Our goal is to develop a theory of approximation, allowing verification procedures to quantify judgements, on how suitable a model is for a given specification — hence mitigating the usual harsh distinction between satisfactory and non-satisfactory system designs. This information, among other things, allows us to evaluate the robustness of our framework, by studying how small changes to our models affect the verification results.
A key source of motivation for this work can be found in The Embedded Systems Design Challenge [HS06] posed by Thomas A. Henzinger and Joseph Sifakis. It contains a call for advances in the state-of-the-art of systems verification, in terms of a new mathematical basis for systems modeling which can incompas behavioural properties as well as environmental constraints. They continue by pointing out that, continuous performance and robustness measures are paramount when dealing with physical resource levels such as clock frequency, energy consumption, latency, mean-time to failure, and cost. For systems integrated in mass-market products, the ability to quantify trade-offs between performance and robustness, under given technical and economic constraints, is of strategic importance.
OriginalsprogEngelsk
ForlagDepartment of Computer Sciences
Antal sider170
StatusUdgivet - 2013
NavnPublication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University
ISSN1601-0590

Fingerprint

Systems analysis
Specifications
Mobile phones
Embedded systems
Websites
Clocks
Energy utilization
Semantics
Hardware
Control systems
Economics
Costs

Citer dette

Thrane, C. (2013). Quantitative Models and Analysis for Reactive Systems. Department of Computer Sciences. Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University
Thrane, Claus. / Quantitative Models and Analysis for Reactive Systems. Department of Computer Sciences, 2013. 170 s. (Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University).
@phdthesis{0f7dcb805f0648ebbc91b157b6d4ef8e,
title = "Quantitative Models and Analysis for Reactive Systems",
abstract = "The majority of modern software and hardware systems are reactive systems, where input provided by the user (possibly another system) and the output of the system is exchanged continuously throughout the (possibly) indefinite execution of the system. Natural examples include control systems, mobile phones and websites.Acknowledging that now more than ever, systems come in contact with the physical world, we need to revise the way we construct models and verification algorithms, to take into account the behavior of systems in the presence of approximate, or quantitative information, provided by the environment in which they are embedded.This thesis studies the semantics and properties of a model-based framework for re- active systems, in which models and specifications are assumed to contain quantifiable information, such as references to time or energy. Our goal is to develop a theory of approximation, allowing verification procedures to quantify judgements, on how suitable a model is for a given specification — hence mitigating the usual harsh distinction between satisfactory and non-satisfactory system designs. This information, among other things, allows us to evaluate the robustness of our framework, by studying how small changes to our models affect the verification results.A key source of motivation for this work can be found in The Embedded Systems Design Challenge [HS06] posed by Thomas A. Henzinger and Joseph Sifakis. It contains a call for advances in the state-of-the-art of systems verification, in terms of a new mathematical basis for systems modeling which can incompas behavioural properties as well as environmental constraints. They continue by pointing out that, continuous performance and robustness measures are paramount when dealing with physical resource levels such as clock frequency, energy consumption, latency, mean-time to failure, and cost. For systems integrated in mass-market products, the ability to quantify trade-offs between performance and robustness, under given technical and economic constraints, is of strategic importance.",
author = "Claus Thrane",
year = "2013",
language = "English",
series = "Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University",
publisher = "Department of Computer Sciences",

}

Thrane, C 2013, Quantitative Models and Analysis for Reactive Systems. Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University, Department of Computer Sciences.

Quantitative Models and Analysis for Reactive Systems. / Thrane, Claus.

Department of Computer Sciences, 2013. 170 s. (Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University).

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

TY - BOOK

T1 - Quantitative Models and Analysis for Reactive Systems

AU - Thrane, Claus

PY - 2013

Y1 - 2013

N2 - The majority of modern software and hardware systems are reactive systems, where input provided by the user (possibly another system) and the output of the system is exchanged continuously throughout the (possibly) indefinite execution of the system. Natural examples include control systems, mobile phones and websites.Acknowledging that now more than ever, systems come in contact with the physical world, we need to revise the way we construct models and verification algorithms, to take into account the behavior of systems in the presence of approximate, or quantitative information, provided by the environment in which they are embedded.This thesis studies the semantics and properties of a model-based framework for re- active systems, in which models and specifications are assumed to contain quantifiable information, such as references to time or energy. Our goal is to develop a theory of approximation, allowing verification procedures to quantify judgements, on how suitable a model is for a given specification — hence mitigating the usual harsh distinction between satisfactory and non-satisfactory system designs. This information, among other things, allows us to evaluate the robustness of our framework, by studying how small changes to our models affect the verification results.A key source of motivation for this work can be found in The Embedded Systems Design Challenge [HS06] posed by Thomas A. Henzinger and Joseph Sifakis. It contains a call for advances in the state-of-the-art of systems verification, in terms of a new mathematical basis for systems modeling which can incompas behavioural properties as well as environmental constraints. They continue by pointing out that, continuous performance and robustness measures are paramount when dealing with physical resource levels such as clock frequency, energy consumption, latency, mean-time to failure, and cost. For systems integrated in mass-market products, the ability to quantify trade-offs between performance and robustness, under given technical and economic constraints, is of strategic importance.

AB - The majority of modern software and hardware systems are reactive systems, where input provided by the user (possibly another system) and the output of the system is exchanged continuously throughout the (possibly) indefinite execution of the system. Natural examples include control systems, mobile phones and websites.Acknowledging that now more than ever, systems come in contact with the physical world, we need to revise the way we construct models and verification algorithms, to take into account the behavior of systems in the presence of approximate, or quantitative information, provided by the environment in which they are embedded.This thesis studies the semantics and properties of a model-based framework for re- active systems, in which models and specifications are assumed to contain quantifiable information, such as references to time or energy. Our goal is to develop a theory of approximation, allowing verification procedures to quantify judgements, on how suitable a model is for a given specification — hence mitigating the usual harsh distinction between satisfactory and non-satisfactory system designs. This information, among other things, allows us to evaluate the robustness of our framework, by studying how small changes to our models affect the verification results.A key source of motivation for this work can be found in The Embedded Systems Design Challenge [HS06] posed by Thomas A. Henzinger and Joseph Sifakis. It contains a call for advances in the state-of-the-art of systems verification, in terms of a new mathematical basis for systems modeling which can incompas behavioural properties as well as environmental constraints. They continue by pointing out that, continuous performance and robustness measures are paramount when dealing with physical resource levels such as clock frequency, energy consumption, latency, mean-time to failure, and cost. For systems integrated in mass-market products, the ability to quantify trade-offs between performance and robustness, under given technical and economic constraints, is of strategic importance.

M3 - Ph.D. thesis

T3 - Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University

BT - Quantitative Models and Analysis for Reactive Systems

PB - Department of Computer Sciences

ER -

Thrane C. Quantitative Models and Analysis for Reactive Systems. Department of Computer Sciences, 2013. 170 s. (Publication : Department of Computer Science, The Faculty of Engineering and Science, Aalborg University).