CS 580 Alloy TutorialSession 1: Intro and LogicGreg Dennis and Rob SeaterSoftware Design Group, MITUsed and modified with permission by Robert StehwienagendaM.C. Escher●Session 1: Intro & Logic●Session 2: Language & Analysis●Session 3: Static Modeling●Session 4: Dynamic Modelingtrans-atlantic analysisOxford, home of ZPittsburgh, home of SMV●notation inspired by Z–sets and relations–uniformity–but not easily analyzed●analysis inspired by SMV–billions of cases in seconds–counterexamples not proofs–but not declarativewhy declarative design?I conclude there are two ways of constructing a software design.One way is to make it so simple there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies. – Tony Hoare [Turing Award Lecture, 1980]why automated analysis?The first principle is that you must not fool yourself, and you are the easiest person to fool.– Richard P. Feynmanalloy case studies●Multilevel security (Bolton)●Multicast key management (Taghdiri)●Rendezvous (Jazayeri)●Firewire (Jackson)●Intentional naming (Khurshid)●Java views (Waingold)●Access control (Zao)●Proton therapy (Seater, Dennis)●Chord peer-to-peer (Kaashoek)●Unison file sync (Pierce)●Telephone switching (Zave)Alloy – Why was it created?●Lightweight –small and easy to use, and capable of expressing common properties tersely and naturally●Precise–having a simple and uniform mathematical semantics●Tractable–amenable to efficient and fully automated semantic analysisAlloy – What is it used for?●Alloy supports high-level semantic object modeling–“object modeling” != “object oriented code design” –“object modeling” means modeling with entities where identity is a primitive notion (not exact)●Alloy is meant for modeling relationships and constraints between basic semantic entities●Alloy is not meant for modeling code architecture (ala class diagrams in UML) although there might be a close relationship between the Alloy specification and an implementation in an OO language–Alloy does not provide method encapsulation and there are no true scalars (only sets)Alloy - Comparison●UML–Has similarities (graphical notation, OCL constraints) but it is neither lightweight, nor precise–UML includes many modeling notions omitted from Alloy (use-cases, state-charts, code architecture specs)–Alloy’s diagrams and relational navigation are inspired by UML●Z–Precise, but intractable. Stylized typography makes it harder to work with.–Z is more expressive than Alloy, but more complicated–Alloy’s set-based semantics is inspired by Zfour key ideas . . .1) everything is a relation2) non-specialized logic3) counterexamples & scope4) analysis by SAT1) everything's a relation●Alloy uses relations for–all datatypes – even sets, scalars, tuples–structures in space and time●key operator is dot join–relational join–field navigation–function applications1why relations?There is no problem in computer science that cannot be solved by an extra level of indirection.– David Wheeler●easy to understand–binary relation is a graph or mapping●easy to analyze–first order (tractable)●uniformWheeler2) non-specialized logic●No special constructs for state machines, traces, synchronization, concurrency . . .3) counterexamples & scopetesting:a few cases of arbitrary sizescope-complete:all cases within a small bound●observations about design analysis:–most assertions are wrong–most flaws have small counterexamples4) analysis by SATStephen CookEugene GoldbergSharad MalikHenry Kautz●Find examples and counterexamples through boolean satisfiability●http://en.wikipedia.org/wiki/Boolean_satisfiability_problem●SAT, the quintessential hard problem (Cook 1971)–SAT is hard, so reduce SAT to your problem●SAT, the universal constraint solver (Kautz, Selman, ... 1990's)–SAT is easy, so reduce your problem to SAT–solvers: Chaff (Malik), Berkmin (Goldberg & Novikov), ...YakovNovikovMoore's LawSAT performanceinstall the Alloy Analyzer - exercise●requires Java 1.4 Runtime Environment–http://java.sun.com➢download the Alloy Analyzer–http://alloy.mit.edu➢run the Analyzer–double click alloy.jar or–execute java -jar alloy.jar at the command line➢this bullet indicates something you should doverify the installation - exercise➢open examples/toys/ceilingsAndFloors.als➢click the “Build” icon–output reads “Compilation successful”➢click the “Execute” icon–output shows graphic●need troubleshooting?–http://alloy.mit.edu/downloads.phpmodeling “ceilings and floors”sig Platform {}there are “Platform” thingssig Man {ceiling, floor: Platform}each Man has a ceiling and a floor Platformpred Above(m, n: Man) {m.floor = n.ceiling}Man m is “above” Man n if m's floor is n's ceilingfact {all m: Man | some n: Man | Above (n,m)}"One Man's Ceiling Is Another Man's Floor"checking “ceilings and floors”assert BelowToo { all m: Man | some n: Man | Above (m,n)}"One Man's Floor Is Another Man's Ceiling"?check BelowToo for 2check "One Man's Floor Is Another Man's Ceiling"counterexample with 2 or less platforms and men?●clicking “Execute” ran this command–counterexample found, shown in graphiccounterexample to “BelowToo”McNaughtonAlloy = logic + language + analysis●logic–first order logic + relational calculus●language–syntax for structuring specifications in the logic●analysis–bounded exhaustive search for counterexample to a claimed property using SATsoftware abstractionslogic: relations of atoms●atoms are Alloy's primitive entities–indivisible, immutable, uninterpreted●relations associate atoms with one another–set of tuples, tuples are sequences of atoms●every value in Alloy logic is a relation!–relations, sets, scalars all the same thinglogic: everything's a relation●sets are unary (1 column) relations Name = {(N0), Addr = {(A0), Book = {(B0), (N1), (A1), (B1)} (N2)} (A2)}●scalars are singleton sets myName = {(N1)} yourName = {(N2)} myBook = {(B0)}●binary relation names = {(B0, N0), (B0, N1), (B1, N2)}●ternary relation addrs = {(B0, N0, A0), (B0, N1, A1), (B1, N1, A2), (B1, N2, A2)}logic: relations●rows are unordered●columns are ordered but unnamed●all