Name
Title | ||
|---|---|---|
Combining formal verification with observed system execution behavior to tune system parameters |
Abstract | ||
|---|---|---|
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 execution will result in a feedback loop that enables model refinement and further optimization of policies and parameters. We demonstrate the applicability of this approach to the adaptive provisioning of resource-limited distributed real-time systems using a multi-mode multimedia case study. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-75454-1_19 | FORMATS |
Keywords | Field | DocType |
system evolves dynamically,system parameter,formal specification,executable formal specification,observed system execution behavior,system execution,dynamic adaptation,on-the-fly formal verification,formal analysis,real-time system,system designer,operating system,resource manager,quantitative analysis,feedback loop,statistical model,middleware,distributed system,study design,formal verification,system design | Resource management,Middleware,Effect system,Computer science,Formal specification,Feedback loop,Formal methods,Executable,Formal verification,Distributed computing | Conference |
Volume | ISSN | ISBN |
4763 | 0302-9743 | 3-540-75453-9 |
Citations | PageRank | References |
9 | 0.52 | 17 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Minyoung Kim | 1 | 202 | 14.56 |
| Mark-oliver Stehr | 2 | 377 | 29.62 |
| Carolyn Talcott | 3 | 1922 | 168.73 |
| Nikil Dutt | 4 | 4960 | 421.49 |
| Nalini Venkatasubramanian | 5 | 232 | 15.42 |