Map
Index
Random
Help
Topics
th

Topic: safety, liveness, and system properties

topics > computer science > programming > Group: program proving



Topic:
automated tests of specifications and designs
Topic:
consistency testing
Topic:
deadlocks
Topic:
debugging by usage rules
Topic:
flavor analysis and typestates for supplementary type checking
Topic:
hard real time systems
Topic:
model checker
Topic:
mobile code
Topic:
path expression
Topic:
program proof via assertions
Topic:
proof-carrying code
Topic:
proving concurrent programs
Topic:
requirement specification by behaviors
Topic:
safe use of pointers
Topic:
specification and design of distributed systems
Topic:
temporal relationships
Topic:
type reflection and introspection
Subtopic: system properties up

Quote: for concurrent programming, prove that bad things can't happen and good things do; i.e., an expression of the program's variables; avoids process interleavings [»schnFB4_1998]
Quote: desired properties for state machines--absence of deadlock, completeness, and liveness; catch basic flaws and unwarranted assumptions [»holzGJ5_1999]

Subtopic: safety and liveness up

Quote: liveness is much harder to prove than safety, yet it is just as important; must prove that g() terminates to prove that h() occurs in f;g;h [»cookB1_2007]
Quote: want to prove safety properties (e.g., no incorrect output) and liveness properties (e.g., termination of program) [»lampL_1980]
Quote: reason about concurrent systems using safety (nothing bad can happen) and progress (something good will happen) assertions [»shanAU9_1993]
Quote: both termination and garbage collection satisfy safety (if marked, it is terminated/garbage) and liveness (will mark if terminated/garbage) [»telG1_1993]
Quote: use invariants for safety properties, and leads-to and invariants for progress properties; includes every property for state-event sequences [»shanAU9_1993]

Subtopic: kill-safe up

Quote: an operation is kill-safe if it is atomic despite thread termination [»flatM6_2004]
Quote: how to extend a run-time system for kill-safe operations; only trusting the shared object

Subtopic: type safety up

Quote: efficient type safety with CCured -- 3-87% time overhead, 1-284% space overhead; Purify and Valgrind are 5x to 130x slower [»necuGC5_2005]

Subtopic: proof rules up

Quote: prove that each component behaves correctly in isolation when its environment is correct; then proof rule for composition under safety and liveness conditions [»abadM1_1993]

Subtopic: safety up

Quote: a safety assertion is a behavioral invariant that is derivable from the specified modes and mode transitions; checked [»atleJM1_1993]
Quote: safety properties are closed under behavior prefixes and stuttering [»abadM1_1993]
Quote: used a model checker to verify safety assertions written in temporal logic; found subtle discrepancies [»atleJM1_1993]
Quote: safety is a quality of the system in which the software is used; it is not a quality of the software itself; reused software may be unsafe [»leveNG7_1993]

Subtopic: liveness up

Quote: a liveness property includes continuations for every finite behavior [»abadM1_1993]
Quote: progress assertions are of the form 'P leads-to Q' where P and Q are predicates; no time bound is implied, but holds when system at rest [»shanAU9_1993]
Quote: to prove liveness properties such as termination need to prove safety properties such as monotonic decreases [»lampL_1980]
Quote: specify liveness axioms by temporal logic; uses box for henceforth and diamond for eventually; defines leads_to [»lampL1_1989]
Quote: automatic prover for liveness properties; extension of fair termination prover; handles large systems written in C [»cookB1_2007]
Quote: specify fair termination using Streett automata; fair non-termination iff either first Boolean succeeds only finitely often, or the second succeeds infinitely often [»cookB1_2007]

Subtopic: synchronization fault up

Quote: bug detectors for thread correctness, performance issue, security violation, usage bug, dropped exception, null pointer, open stream, unchecked return, unconditional wait
[»hoveD12_2004]

Related Topics up

Topic: automated tests of specifications and designs (12 items)
Topic: consistency testing (60 items)
Topic: deadlocks (21 items)
Topic: debugging by usage rules (41 items)
Topic: flavor analysis and typestates for supplementary type checking (68 items)
Topic: hard real time systems (64 items)
Topic: model checker (49 items)
Topic: mobile code (14 items)
Topic: path expression (14 items)
Topic: program proof via assertions (61 items)
Topic: proof-carrying code (7 items)
Topic: proving concurrent programs (37 items)
Topic: requirement specification by behaviors (16 items)
Topic: safe use of pointers (102 items)
Topic: specification and design of distributed systems (14 items)
Topic: temporal relationships (40 items)
Topic: type reflection and introspection
(28 items)

Updated barberCB 4/05
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.