Formal Verification – Real-time Systems MCQs

50 min
Score: 0
Attempted: 0/50
Subscribe

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