1. What is formal verification in real-time systems?
(A) Mathematical verification of system correctness
(B) Manual code inspection
(C) Performance testing
(D) Debugging technique
2. Formal verification primarily relies on:
(A) Testing scenarios
(B) Simulation
(C) Mathematical models
(D) User feedback
3. Which system property ensures that nothing bad ever happens?
(A) Safety
(B) Timeliness
(C) Liveness
(D) Fairness
4. Which property ensures that something good eventually happens?
(A) Liveness
(B) Safety
(C) Reliability
(D) Availability
5. What is the main goal of formal verification?
(A) Guaranteed correctness of system behavior
(B) Faster execution
(C) Reduced memory usage
(D) Easier debugging
6. Which technique is commonly used in formal verification of real-time systems?
(A) Unit testing
(B) Model checking
(C) Code refactoring
(D) Profiling
7. Which formal model explicitly represents time?
(A) Finite automata
(B) Petri nets
(C) Timed automata
(D) Pushdown automata
8. What is a specification in formal verification?
(A) Implementation code
(B) Informal requirement
(C) Test case
(D) Formal description of desired properties
9. Which logic is often used to specify real-time properties?
(A) Propositional logic
(B) First-order logic
(C) Boolean algebra
(D) Temporal logic
10. Which temporal logic extends CTL with time constraints?
(A) LTL
(B) PLTL
(C) TCTL
(D) FOL
11. What does a counterexample represent?
(A) Violation of specification
(B) Correct execution trace
(C) Optimization result
(D) Successful proof
12. Which verification technique explores all reachable states?
(A) Simulation
(B) Testing
(C) Debugging
(D) Model checking
13. What is a major challenge in formal verification?
(A) Syntax errors
(B) State space explosion
(C) Compilation delay
(D) Code readability
14. Which abstraction technique reduces state space size?
(A) Scheduling
(B) Logging
(C) Symbolic abstraction
(D) Monitoring
15. Which property ensures tasks meet deadlines?
(A) Safety
(B) Timeliness
(C) Liveness
(D) Fairness
16. Which formal method uses proofs to verify correctness?
(A) Model checking
(B) Simulation
(C) Theorem proving
(D) Testing
17. Which is an advantage of model checking over testing?
(A) Exhaustive verification
(B) Faster execution
(C) Easier coding
(D) Lower memory usage
18. Which tool is widely used for real-time formal verification?
(A) UPPAAL
(B) MATLAB
(C) GCC
(D) Eclipse
19. What does formal verification guarantee if successful?
(A) Absence of specified errors
(B) Optimal performance
(C) Faster response
(D) Minimal power usage
20. Which system is suitable for formal verification?
(A) Simple scripts
(B) Web browsers
(C) Text editors
(D) Safety-critical real-time systems
21. Which formal logic is used for branching-time properties?
(A) LTL
(B) Propositional logic
(C) FOL
(D) CTL
22. What is a run in formal verification models?
(A) Compilation phase
(B) Execution trace of the system
(C) Debugging step
(D) Test input
23. Which technique verifies correctness using invariants?
(A) Simulation
(B) Theorem proving
(C) Runtime monitoring
(D) Testing
24. Which real-time constraint can be formally verified?
(A) Code readability
(B) Memory alignment
(C) User interface quality
(D) Deadline satisfaction
25. Which formal model is suitable for concurrency?
(A) Sequential automata
(B) Linear programs
(C) Timed automata
(D) Scripts
26. Which verification method provides counterexamples?
(A) Theorem proving
(B) Model checking
(C) Code review
(D) Simulation
27. Which aspect distinguishes formal verification from testing?
(A) Uses test cases
(B) Partial coverage
(C) Mathematical rigor
(D) Execution speed
28. What is soundness in formal verification?
(A) Faster execution
(B) Easier debugging
(C) Reduced memory usage
(D) All verified properties are correct
29. Which verification checks worst-case timing behavior?
(A) Timing verification
(B) Functional verification
(C) Memory verification
(D) Power verification
30. Which problem arises due to parallel components?
(A) Syntax error
(B) Power loss
(C) Compilation delay
(D) State explosion
31. Which approach combines testing with formal methods?
(A) Manual inspection
(B) Compilation
(C) Debugging
(D) Runtime verification
32. Which formal method verifies infinite-state systems symbolically?
(A) Explicit-state checking
(B) Symbolic model checking
(C) Manual proof
(D) Testing
33. Which structure is used in symbolic model checking?
(A) Stack
(B) Queue
(C) Binary Decision Diagrams
(D) Arrays
34. Which property ensures no starvation occurs?
(A) Safety
(B) Liveness
(C) Fairness
(D) Timeliness
35. Which system behavior is verified by safety properties?
(A) Absence of catastrophic states
(B) Eventual response
(C) Deadline satisfaction
(D) Resource utilization
36. Which logic is used for linear-time properties?
(A) CTL
(B) LTL
(C) TCTL
(D) FOL
37. Which real-time system requires strict formal verification?
(A) Gaming application
(B) Media player
(C) Text editor
(D) Medical device controller
38. Which verification ensures system never enters an error state?
(A) Safety
(B) Liveness
(C) Fairness
(D) Timeliness
39. What does abstraction preserve in formal verification?
(A) Performance
(B) Essential properties
(C) Code structure
(D) User interface
40. Which method checks correctness without executing the system?
(A) Testing
(B) Simulation
(C) Formal verification
(D) Debugging
41. Which is a limitation of formal verification?
(A) Lack of rigor
(B) High computational cost
(C) Low accuracy
(D) Unclear results
42. Which verification technique is interactive?
(A) Model checking
(B) Theorem proving
(C) Testing
(D) Simulation
43. Which concept defines allowable system behaviors?
(A) Implementation
(B) Debugger
(C) Compiler
(D) Specification
44. Which real-time logic supports deadlines?
(A) LTL
(B) CTL
(C) TCTL
(D) FOL
45. Which benefit does formal verification provide?
(A) Guaranteed correctness w.r.t specification
(B) Faster execution
(C) Reduced development time
(D) Easier coding
46. Which verification ensures all paths satisfy a property?
(A) Existential
(B) Probabilistic
(C) Universal
(D) Random
47. Which formal method is best for safety-critical timing analysis?
(A) Model checking
(B) Simulation
(C) Code review
(D) Profiling
48. Which artifact is produced when verification fails?
(A) Counterexample
(B) Test report
(C) Executable code
(D) Optimization log
49. Which property ensures bounded response time?
(A) Safety
(B) Liveness
(C) Fairness
(D) Timeliness
50. Formal verification in real-time systems focuses on:
(A) Mathematical correctness of time-constrained behavior
(B) User satisfaction
(C) Graphical design
(D) Hardware speed