1. What is the primary purpose of model checking in real-time systems?
(A) Code generation
(B) Performance optimization
(C) Automatic verification of system properties
(D) Hardware synthesis
2. Model checking is mainly used to verify:
(A) Coding style
(B) User interface design
(C) Logical correctness of specifications
(D) Power consumption
3. Which property ensures that “nothing bad ever happens”?
(A) Liveness
(B) Fairness
(C) Safety
(D) Timeliness
4. Which property ensures that “something good eventually happens”?
(A) Safety
(B) Liveness
(C) Deadlock
(D) Reachability
5. What is a state in model checking?
(A) A program variable
(B) A snapshot of system variables
(C) A compiler phase
(D) A scheduling algorithm
6. Which technique systematically explores all possible states?
(A) Simulation
(B) Testing
(C) Debugging
(D) Model checking
7. Which is a major challenge in model checking?
(A) Syntax errors
(B) State space explosion
(C) Compilation time
(D) Memory leaks
8. Which formal model is commonly used in real-time model checking?
(A) Timed automata
(B) Flowcharts
(C) ER diagrams
(D) Decision trees
9. What does reachability analysis determine?
(A) Maximum execution time
(B) Memory size
(C) Whether a state can be reached
(D) Processor speed
10. Which logic is commonly used to specify properties in model checking?
(A) Boolean logic
(B) Predicate logic
(C) Fuzzy logic
(D) Temporal logic
11. Which temporal logic is specifically designed for real-time systems?
(A) LTL
(B) CTL
(C) Propositional logic
(D) TCTL
12. What does CTL stand for?
(A) Computation Tree Logic
(B) Continuous Time Logic
(C) Computation Time Logic
(D) Concurrent Task Logic
13. Which of the following is a real-time property?
(A) Variable initialization
(B) Memory alignment
(C) Code reuse
(D) Deadline satisfaction
14. What is a counterexample in model checking?
(A) Execution trace violating a property
(B) Proof of correctness
(C) Correct execution trace
(D) Optimization result
15. Which approach reduces state space size?
(A) Overclocking
(B) Abstraction
(C) Profiling
(D) Logging
16. Which technique groups similar states together?
(A) Scheduling
(B) Testing
(C) Debugging
(D) Symbolic model checking
17. What structure is commonly used in symbolic model checking?
(A) Binary Decision Diagrams
(B) Arrays
(C) Linked lists
(D) Stacks
18. Which type of system benefits most from model checking?
(A) Static websites
(B) Text editors
(C) Word processors
(D) Real-time embedded systems
19. What does real-time model checking add compared to classical model checking?
(A) Memory analysis
(B) User interaction
(C) Code generation
(D) Explicit time constraints
20. Which tool supports real-time model checking?
(A) GCC
(B) Eclipse
(C) MySQL
(D) UPPAAL
21. What is the role of a specification in model checking?
(A) Execute code
(B) Define desired properties
(C) Optimize memory
(D) Schedule tasks
22. Which system behavior is verified by safety properties?
(A) Deadlines always met
(B) Eventual response
(C) Absence of catastrophic states
(D) Fair scheduling
23. What does liveness guarantee?
(A) No bad state occurs
(B) CPU is idle
(C) Memory is freed
(D) System eventually progresses
24. Which method explores states on-the-fly?
(A) On-the-fly model checking
(B) Simulation
(C) Static analysis
(D) Profiling
25. Which factor causes infinite state spaces in real-time systems?
(A) Continuous time
(B) Finite memory
(C) Limited clocks
(D) Static scheduling
26. Which abstraction is used for clocks in real-time model checking?
(A) Data abstraction
(B) Memory abstraction
(C) Zone abstraction
(D) Control abstraction
27. Which analysis checks if a property holds on all execution paths?
(A) Existential
(B) Probabilistic
(C) Random
(D) Universal
28. Which type of error can model checking detect?
(A) Syntax error
(B) Typographical error
(C) Timing violation
(D) Formatting error
29. What is deadlock detection used for?
(A) Identifying states with no outgoing transitions
(B) Improving speed
(C) Code optimization
(D) Memory allocation
30. Which property ensures tasks complete within deadlines?
(A) Safety
(B) Timeliness
(C) Liveness
(D) Fairness
31. Which of the following is NOT a model checking technique?
(A) Explicit-state model checking
(B) Symbolic model checking
(C) Statistical model checking
(D) Manual code review
32. What does explicit-state model checking store?
(A) All reachable states explicitly
(B) Logical formulas
(C) Code comments
(D) Scheduling tables
33. Which logic uses path quantifiers and temporal operators?
(A) CTL
(B) Propositional logic
(C) First-order logic
(D) Boolean algebra
34. Which approach handles probabilistic timing behavior?
(A) Probabilistic model checking
(B) Deterministic checking
(C) Symbolic execution
(D) Static analysis
35. Which model checking tool supports probabilistic real-time systems?
(A) SPIN
(B) UPPAAL
(C) PRISM
(D) NS-2
36. Which real-time system property is time-bounded?
(A) Memory safety
(B) Code correctness
(C) Deadline compliance
(D) Resource sharing
37. What is the main benefit of counterexamples?
(A) Improve performance
(B) Increase abstraction
(C) Help locate design errors
(D) Reduce memory usage
38. Which operation is checked during model checking?
(A) Compilation
(B) State transition
(C) File I/O
(D) Code formatting
39. What does fairness ensure?
(A) Equal memory usage
(B) Fast execution
(C) No starvation of enabled actions
(D) Minimal states
40. Which model represents concurrent behaviors?
(A) Sequential model
(B) Functional model
(C) Linear model
(D) State-transition model
41. Which property checks that a system never reaches an error state?
(A) Safety
(B) Liveness
(C) Reachability
(D) Fairness
42. What is the input to a model checker?
(A) Formal system model and properties
(B) Executable code
(C) Test cases
(D) Debug logs
43. Which system is verified exhaustively by model checking?
(A) Abstract finite-state model
(B) Infinite real system
(C) Hardware prototype
(D) User manual
44. Which logic is suitable for branching-time properties?
(A) CTL
(B) LTL
(C) TCTL
(D) Propositional logic
45. What does statistical model checking rely on?
(A) Exhaustive exploration
(B) Random simulation runs
(C) Manual inspection
(D) Code profiling
46. Which real-time verification checks minimum and maximum delays?
(A) Safety analysis
(B) Timing analysis
(C) Memory analysis
(D) Power analysis
47. Which problem arises due to concurrency in real-time systems?
(A) Syntax ambiguity
(B) Compilation error
(C) Code duplication
(D) State explosion
48. What does model checking guarantee if a property is satisfied?
(A) Code efficiency
(B) Reduced power usage
(C) Faster execution
(D) Logical correctness w.r.t. the model
49. Which verification result indicates success?
(A) Counterexample found
(B) Property violated
(C) State unreachable
(D) Property satisfied
50. Model checking is best described as:
(A) Dynamic testing technique
(B) Formal verification technique
(C) Code optimization method
(D) Debugging approach