Sciweavers

Share
FORMATS
2007
Springer

Combining Formal Verification with Observed System Execution Behavior to Tune System Parameters

10 years 5 months ago
Combining Formal Verification with Observed System Execution Behavior to Tune System Parameters
Resource limited DRE (Distributed Real-time Embedded) systems can benefit greatly from dynamic adaptation of system parameters. We propose a novel approach that employs iterative tuning using light-weight, on-the-fly formal verification with feedback for dynamic adaptation. One objective of this approach is to enable system designers to analyze designs in order to study design tradeoffs across multiple layers (for example, application, middleware, operating system) and predict the possible property violations as the system evolves dynamically over time. Specifically, an executable formal specification is developed for each layer of the distributed system under consideration. The formal specification is then analyzed using statistical model checking and statistical quantitative analysis, to determine the impact of various resource management policies for achieving desired end-to-end timing/QoS properties. Finally, integration of formal analysis with dynamic behavior from system executio...
Minyoung Kim, Mark-Oliver Stehr, Carolyn L. Talcot
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where FORMATS
Authors Minyoung Kim, Mark-Oliver Stehr, Carolyn L. Talcott, Nikil Dutt, Nalini Venkatasubramanian
Comments (0)
books