[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

JacksonD00

  1. Daniel Jackson
  2. Automating first-Order Relational Logic

    [FSE8] pp120-139

  3. =THEORY LOGIC RELATIONS PREDICATE Z OCL =DEMO TOOL 50KLOC Java SAT Alloy Analyzer Nitpick UML COM Mobile IP
  4. Shorter than SMV by 10 times.
  5. Quantifiers make logic easier to use. Analysis s faster than Nitpick as well.
  6. Describes syntax, type rules and semantics of the logic.
  7. In place of composition of relations ( R; S = rel[x,z](some y, x R y S z)), defines navigation ( R . S = rel[x,z](some y, y R z and y S x))
  8. scalar variables are replaced by singleton set variables.
  9. analysis:= normalize and skolemize; boolean formula; conjunctive normal form; SAT solver; map back to relational.
  10. Alloy_Analyzer::= See http://sdg.lcs.mit.edu/alloy
  11. Proved UML meta-model is consistent in less than 20 seconds.
  12. See also [JacksonDSullivan00]

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]