Topic: model checker

topics > computer science > programming > Group: testing

program proving

automated testing
automated tests of specifications and designs
code optimization by global analysis
communication protocols
compiler error checking
consistency testing
debugging by usage rules
debugging techniques
event controlled processing
flavor analysis and typestates for supplementary type checking
formal methods and languages
reliable communication
program proof via assertions
program proving is infeasible
proving concurrent programs
requirement specification by behaviors
safety, liveness, and system properties
specification and design of distributed systems
state machine
symbolic execution
temporal relationships
type-safe and secure languages


An alternative to symbolic execution by Henderson et al (ph75) is describing the program by a symbolic model based on state definitions. Their TOPD system symbolically executes this model during testing and development, then code is generated by paraphrase extension. (cbb 5/80)
Subtopic: compute power up

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

Subtopic: bug finding up

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]

Subtopic: safety and liveness up

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

Subtopic: abstract model up

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]

Subtopic: model programs as a state machine up

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]

Subtopic: model as part of program up

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]

Subtopic: protocol verification up

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]

Subtopic: verifying distributed systems up

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]

Subtopic: bitstate verification up

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

Subtopic: writing requirements up

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]

Subtopic: test harnass for event-driven code up

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]

Subtopic: binary decision diagram up

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

Subtopic: temporal logic up

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)

Subtopic: simplifying model checkers up

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

Subtopic: debugging models up

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]

Subtopic: implementation up

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

Subtopic: example up

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]

Subtopic: problems with model checker up

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

Related Topics up

Group: formalism   (9 topics, 478 quotes)
Group: program proving   (10 topics, 311 quotes)

Topic: automated testing (25 items)
Topic: automated tests of specifications and designs (12 items)
Topic: code optimization by global analysis (24 items)
Topic: communication protocols (62 items)
Topic: compiler error checking (16 items)
Topic: consistency testing (60 items)
Topic: debugging by usage rules (41 items)
Topic: debugging techniques (23 items)
Topic: event controlled processing (46 items)
Topic: flavor analysis and typestates for supplementary type checking (68 items)
Topic: formal methods and languages (53 items)
Topic: reliable communication (29 items)
Topic: program proof via assertions (61 items)
Topic: program proving is infeasible (47 items)
Topic: proving concurrent programs (37 items)
Topic: requirement specification by behaviors (16 items)
Topic: safety, liveness, and system properties (22 items)
Topic: specification and design of distributed systems (14 items)
Topic: state machine (67 items)
Topic: symbolic execution (9 items)
Topic: temporal relationships (40 items)
Topic: type-safe and secure languages
(43 items)

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