Real-time constraints
Quantitative timing analysis
Research questions: How can we extend this technique to continuous time How can we deal with dynamic process creation and deletion
Modeling the Environment
Hybrid dynamics
Dealing with both discrete and continuous state variables
Research question: How can we automate and scale differential equations models for large systems
Stochastic models
Dealing with uncertainty, unpredictability
Using continuous variables (e.g., probabilities) for reliability and cost-benefit analyses
Research questions: How can we handle dependent events, cascading of events Both nondeterministic and probabilistic state transitions
Usability
Extracting models
Synchronization skeletons
Translators for task execution languages
Research question: How can we balance expressibility of languages with efficiency of verification and user-friendliness
Explaining verification tool results
Adopt AI techniques to explain counterexamples for task executive programs.
Develop techniques to view and browse the temporal evolution of counterexamples.
Research question: How can we create virtual execution traces that can be used by existing visualization tools
The Rare Glitch Tool Suite
…
Prism
Checkmate
PVS
Symp
SMV
Specification
Model
Counter-
examples
Checkers and Provers
Specification and Modeling Languages
Analysis Engines
Reliability and Cost Analyzers
Explanation Generator
Abstraction/Refinement Processor
…
Preliminary Planning
Technical
So far: Technical presentations of our current work

上一页下一页