tractable object models Daniel Jackson Software Design Group MIT Laboratory for Computer Science WG 2.9 ∑ Flims ∑ February 7, 2000

2/16/00


Click here to start


Table of Contents

tractable object models Daniel Jackson Software Design Group MIT Laboratory for Computer Science WG 2.9 ∑ Flims ∑ February 7, 2000

lightweight formal methods

progress

semantic minimalism

relational structure

example

modelling implication

partial function problem

my approach

an example

basic notions

object model diagram

Alloy model: declarations

an indicative invariant

a safety condition

two definitions

policy invariants

an operation

analysis strategy

bug example, inconsistency

bug example, implication

output

bug example, preservation of invariant

funky overlap

why itís hard (1)

small scope hypothesis

why itís hard (2)

translating to SAT

research status

conclusion

Author: Daniel Jackson

Email: dnj@lcs.mit.edu

Home Page: http://sdg.lcs.mit.edu/~dnj

Download presentation source