| 
|
QuoteRef: abadM1_1993
topics >
all references >
ThesaHelp:
ACM references a-e
ThesaHelp:
references a-b
Topic:
abstraction in programming
Topic:
safety, liveness, and system properties
Topic:
proving concurrent programs
Topic:
state machine
Topic:
requirement specification by behaviors
Topic:
Petri net
Group:
requirement specification
Topic:
evaluation in an environment
Group:
program proving
Reference
Abadi, M., Lamport, L., "Composing specifications", ACM Transactions on Programming Languages and Systems, 15, 1, January 1993, pp. 73-132. Google
abstract ;;Quote: prove that each component behaves correctly in isolation when its environment is correct; then proof rule for composition under safety and liveness conditions
73 ;;Quote: transition-axiom method for proving concurrent systems combines abstract programs and temporal logic; rules for implementation and composition
77 ;;Quote: a system behavior is an alternating sequence of states (interface) and agents (system or environment)
77+;;Quote: a specification is a formal description of the interface between a system and its environment
83 ;;Quote: a specification is realizable iff the system has a winning strategy; i.e., the system wins under all legal environment behaviors
78 ;;Quote: a property is a set of system behaviors; verify for each possible system execution
81 ;;Quote: safety properties are closed under behavior prefixes and stuttering
81 ;;Quote: a liveness property includes continuations for every finite behavior
106 ;;Quote: used detailed, hierarchical proofs since theorems about concurrent system specifications are difficult to get right
107 ;;Quote: write a detailed, hierarchical proof with a preamble that describes assumptions and why the desired conclusion implies the result
ThesaHelp: ACM references a-e (259 items)
ThesaHelp: references a-b (396 items)
Topic: abstraction in programming (67 items)
Topic: safety, liveness, and system properties (22 items)
Topic: proving concurrent programs (37 items)
Topic: state machine (67 items)
Topic: requirement specification by behaviors (16 items)
Topic: Petri net (44 items)
Group: requirement specification (11 topics, 307 quotes)
Topic: evaluation in an environment (35 items)
Group: program proving (10 topics, 311 quotes)