Temporal-Logic-Based Testing Tool Architecture for Dual-Programming Model Systems