how would model checking differ for software?
sequential
focus not on concurrency
relational
state itself is relational
essence of Z, RDB, OO
incremental & modular
global operations
declarative style
abstract
all software is infinite state
Previous slide
Next slide
Back to first slide
View graphic version