Usability
Extracting models
Explaining tool feedback
system
environment
Technical Challenges
Interleavings of multiple task executions
Inter-task dependencies and synchronization requirements
System resource constraints
Hard real-time constraints
Interactions with complex physical dynamic systems
Adverse, unpredictable environments
Stringent requirements for autonomy, fault tolerance, and survivability
Technical Approach
Embedded System
Environment
Design Engineer's Verification Toolbox
Usability
System Integrity Properties
Synchronization Constraints
Real-time Constraints
Resource Constraints
Modeling the Environment
Modeling Uncertainty: Stochastic Models
System-Environment Interactions: Hybrid Dynamics
Foundational Building Blocks
Model checking techniques and tools
Task-level system architecture, task executive languages
Continuous dynamics, quantitative analysis, reliability analysis
Cross-Cutting Themes
Exploit model checking techniques and tools.
Focus on the task level.
Incorporate continuous domains in our models.
Verifying System Integrity
Synchronization constraints
Publish-subscribe architecture
Cyclic-tasks with shared variables
Research question: How can we reason about their aggregate behavior
Resource constraints
Continuous, consumable (e.g., fuel) and renewable (e.g., bandwidth, disk space) resources
Research question: How should we specify and verify resource constraints

上一页下一页