Quote: in 30 years, the size of software increased less than 100x while computing power increased 1,000,000x [»holzGJ11_2002]

Quote: validation methods are primarily used as bug-finders; formal methods are useful because they find different bugs than traditional methods; a more realistic goal than guaranteeing correctness [»dillDL4_1996]

Quote: safety properties such as deadlock and assertions have linear cost in number of reachable states [»holzGJ5_1997]

Quote: liveness properties such as starvation and acceptance cycles take same memory and twice as much time as safety properties

Quote: use predicate abstraction for model checking with symbolic names for values; these models may be reused across multiple applications in an open environment; implemented for boolean abstractions [»ballT3_2005]

Quote: verifying a finite state model is much easier that fully understanding a system's behavior; e.g., only four operations on user IDs [»chenH8_2002]

Quote: the operating system must behave deterministically relative to its finite state model; if not, add global variables to state; each state represented by an equivalence class [»chenH8_2002]

Quote: use finite state model to check proper usage of uid-setting system calls; build a finite state model of the program; check for privileged regions [»chenH8_2002]

Quote: modeling with finite state machines is practical; TOPD discourages elaborate models by full expression of state transitions [»hendP9_1975]

Quote: a verification model must identify control states, event types, and event responses as code fragments [»holzGJ5_1999]

Quote: Metal is a state machine language for analyzing programs; like yacc [»englD10_2001]

Quote: TOPD models a program by a set of abstract values for objects (i.e., states) and the effects of operations (i.e., transitions); used by tester/checker [»hendP9_1975]

Quote: in a TOPD model, an operation's transitions should be defined for every state vector generated by TOPD [»hendP9_1975]

Quote: specification mining analyzes a program's trace of API or ADT calls; produces state machines with temporal and data dependencies [»ammoG1_2002]

Quote: Slam turns a C program into a boolean program with the same control-flow and Boolean variables; easier to analyze [»laruJR5_2004]

Quote: eliminate spurious paths in a Boolean program by automatically adding boolean control variables; e.g., resource allocation within loops and conditionals [»laruJR5_2004]

Quote: event-driven state-machine programming (ESP) for programmable devices; generates a C program and SPIN model; 90% fewer lines of code, low overhead [»kumaS6_2001]

Quote: the ESP compiler extracts Spin models for checking; can often fully debug with the model checker [»kumaS6_2002]

Quote: Lucent uses virtual finite-state machines (VFSM) to separate the control behavior of a software module from its data manipulation; formal, executable, early error checking, 50% fewer defects, automatic documentation [»florAR1_1997]

Quote: the VFSM simulator generates message sequence charts showing states, inputs, outputs, and communications; with seqflow, it documents the behavior of a module [»florAR1_1997]

Quote: rigorous, detailed, readable specification from real-world traces of three implementations of the TCP/IP protocols and Sockets API; verified with a symbolic model checker [»bishS1_2006]

Quote: validated a TCP/IP/Socket specification by model checking actual traces; 97% success for UDP and 91% success for TCP; half of the TCP failures due to test and check problems [»bishS1_2006]

Quote: used SPIN to develop a retransmission protocol; 65 lines test code, all errors identified, 1/5 the development time [»kumaS6_2001]

Quote: reimplemented VMMC using 500 lines of ESP and 3000 lines of C; replaced 15,600 lines; exhaustively checked the ESP code [»kumaS6_2002]

Quote: the VFSM validator exhaustively exercises a network of communicating VFSMs using the supertrace algorithm; found errors in three tested applications; widely used formal method [»florAR1_1997]

Quote: explicit-state model checking with bitstate verification and Bloom filters; e.g., Spin, cache coherence, and network protocols [»dillPC4_2004]

Quote: graphical time-line editor for writing requirements for a logic model checker; a requirement consists of a preamble, a response, constriants, and ignored events [»smitMH8_2001]

Quote: a test harness for event-driven software defines a map of selected source statements, test drivers, and desired properties [»holzGJ5_1999]

Quote: 450 lines of test driver code caught 25 timing-dependent errors; difficult to detect with conventional testing [»holzGJ5_1999]

Quote: the TOPD tester exhaustively executes the model of a procedure; result is state vectors for each valid execution path [»hendP9_1975]

Quote: the TOPD tester annotates the procedure with its state vectors and reports on potential programming errors [»hendP9_1975]

Quote: TOPD's checker generates test cases from the model and determines if the procedure's result matches the model's result [»hendP9_1975]

Quote: use binary decision diagrams (BDD) for subset-based points-to analysis; BDDs from model checking; simple, less space, scales well [»bernM6_2003]

Quote: logic model checking is effective for concurrency-related errors; based on temporal logic as proposed by Pnueli [»holzGJ11_2002]

Quote: the TimeLine graphical editor simplifies the specification of basic temporal properties for SPIN model checkers; linear temporal logic is difficult to use [»holzGJ11_2002]

Quote: use SPIN for design and verification of asynchronous process systems using rendezvous, buffered channels, and/or shared variables; design with PROMELA [»holzGJ5_1997]

Quote: SPIN represents correctness claims in linear temporal logic (LTL)

Quote: efficient algorithm to convert timestamps into event clocks; reduces state space for model checker of distributed protocols [»dereF3_2001]

Quote: order of magnitude faster model checker by pruning similar states; e.g., red-black trees only touch one path in the tree from root to a leaf [»dargPT10_2006]

Quote: SPIN--on-the-fly model checker; partial search with bit-state hashing and simulation mode [»kumaS6_2001]

Quote: SPIN's simulation mode finds the most bugs; random choice at each turn; users rarely find rare bugs

Quote: using correct traces to identify the cause of multiple, erroneous traces of a model checker [»ballT1_2003]

Quote: efficient algorithms to compute the correct traces of a model checker; linear in size of state space [»ballT1_2003]

Quote: TOPD's tester/checker could report which program states matched the predicted ones [»hendP9_1975]

Quote: computing hash values is the most expensive operation in a model checker [»dillPC4_2004]

Quote: formal analysis of a plan execution module for NASA's Remote Agent; first complete, AI control of a space-craft [»haveK8_2001]

Quote: SPIN found five errors in part of the LISP code for NASA's Remote Agent; took 12 man weeks to model and one week to verify [»haveK8_2001]

Quote: model checkers find a few difficult errors with simplified code; meta-level compilation works directly with program source and found many errors [»chouA11_2000]

Quote: modeling with a finite state machine is as difficult as programming; will report inconsistencies between model and implementation [»hendP9_1975]