| 
|
QuoteRef: holzGJ5_1999
topics >
all references >
ThesaHelp:
references g-h
Topic:
state machine
Topic:
model checker
Topic:
constructing proof and program together
Topic:
event controlled processing
Topic:
test scripts
Topic:
safety, liveness, and system properties
Topic:
deadlocks
Topic:
proving concurrent programs
Topic:
device driver
Reference
Holzmann, G.J., Smith, M.H., "A practical method for verifying event-driven software", Proceedings of the 1999 International Conference on Software Engineering (ICSE), Los Angeles, CA, USA, May 1999, pp. 597-607. Google
Other Reference
Holzmann and Smith, "An automated verification method for distributed sysstems software based on model extraction," IEEE Transactions on Software Engineering, 28.4:364-377, April 2002
599 ;;Quote: a verification model must identify control states, event types, and event responses as code fragments
599+;;Quote: use @-format to implement control states in event-driven software; labels to suspend and resume execution
601 ;;Quote: a test harness for event-driven software defines a map of selected source statements, test drivers, and desired properties
602 ;;Quote: desired properties for state machines--absence of deadlock, completeness, and liveness; catch basic flaws and unwarranted assumptions
602 ;;Quote: 450 lines of test driver code caught 25 timing-dependent errors; difficult to detect with conventional testing
ThesaHelp: references g-h (299 items)
Topic: state machine (67 items)
Topic: model checker (49 items)
Topic: constructing proof and program together (22 items)
Topic: event controlled processing (46 items)
Topic: test scripts (13 items)
Topic: safety, liveness, and system properties (22 items)
Topic: deadlocks (21 items)
Topic: proving concurrent programs (37 items)
Topic: device driver (15 items)