| 
|
QuoteRef: atleJM1_1993
topics >
all references >
ThesaHelp:
references a-b
Topic:
requirement specification by behaviors
Topic:
state machine
Topic:
events
Topic:
safety, liveness, and system properties
Topic:
race conditions
Topic:
program proof via assertions
Reference
Atlee, J.M., Gannon, J., "State-based model checking of event-driven system requirements", IEEE Transactions on Software Engineering, 19, 1, pp. 24-40, January 1993. Google
24 ;;Quote: a requirements specification describes a system's modes of operation, events that change modes, and invariant, safety properties
24 ;;Quote: specify requirements by a mode machine; each modeclass describes one aspect of system behavior by modes and transitions
25 ;;Quote: an event is an instantaneous change in an environmental condition; input to a mode-machine
26 ;;Quote: a safety assertion is a behavioral invariant that is derivable from the specified modes and mode transitions; checked
26 ;;Quote: automatically propagate redundant information in a mode transition table; e.g., simultaneous mode transitions
27 ;;Quote: used a model checker to verify safety assertions written in temporal logic; found subtle discrepancies
ThesaHelp: references a-b (396 items)
Topic: requirement specification by behaviors (16 items)
Topic: state machine (67 items)
Topic: events (44 items)
Topic: safety, liveness, and system properties (22 items)
Topic: race conditions (30 items)
Topic: program proof via assertions (61 items)