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...

• Type: Conference
• Year: 2007
• Where: FORMATS
• Authors: Minyoung Kim, Mark-Oliver Stehr, Carolyn L. Talcott, Nikil Dutt, Nalini Venkatasubramanian
• Keywords: Distributed Systems, Dynamic Adaptation, Formal Methods, Formal Specification, FORMATS 2007