How to design software
Daniel Jackson
Expanding Horizons in Computing, MIT
January 29, 2024
Slides
Video All videos from event
I explain how successful innovations in software can usually be traced to just one or two "concepts" that offer new scenarios that, with seemingly small shifts, radically change how an application is used. I give examples from apps such as Zoom, WhatsApp and Calendly. I explain how concepts, each with their own characteristic scenarios, can be composed to form apps. I explain how this idea can be used to make software more usable, modular and consistent.
What is software innovation?
Daniel Jackson
TEDx MIT
December 16, 2023
Slides
Video
What does software innovation look like? In this tiny talk, I argue that it's not about technology breakthroughs, or even radically new ideas. Most often, a software innovation succeeds because it offers a new piece of functionality (aka, a concept) that eliminates some constraint that made previous solutions much less attractive. To show this, I consider four examples of blockbuster innovations—the Web, Apple's iPod, WhatsApp and Zoom—and identify the key concept in each case. The concept can be summarized by an "operational principle" (OP), an archetypal scenario that shows how it's typically used. When you compare the OPs before and after introduction of the key concept, you can see how annoying and burdensome steps are eliminated. These key concepts become what Merrick Furst calls "not nots" (once you know about them, not having them is not ok), which are the essence of authentic demand (as explained in a new book by Merrick and his colleagues).
Why AI needs software design
Daniel Jackson
CSAIL Imagination in Action
June 27, 2023
Video
All videos from event
In this very short talk, I start with three striking examples of recent software failures. I explain that such failures usually happen not because of bugs but because of conceptual mismatches that cause users to issue bad instructions. Then I posit two simple ways in which AI might be integrated into software apps, and argue that in both cases paying attention to the underlying concepts will be key to preventing failures. I close with the idea of a "concept catalog" that draws together concepts across applications so they can be reused.
Software Development in the Age of AI
Daniel Jackson
Opening Keynote, CSAIL Alliances Annual Meeting
May 25, 2023
Slides
How will AI agents, and LLMs like GPT in particular, change the way software is developed? In this talk, I argue that LLMs have some inherent flaws, and that it would be foolish to assume that these will be overcome. On the other hand, their capabilities will grow immensely, so the right question to ask is how a new software development paradigm can be created that capitalizes on these capabilities and minimizes the limitations. I argue that the key elements of such a paradigm are: exploiting familiar forms; relying on domain-specificity; and working in a methodical and granular fashion. I explain how concept design provides the foundation for such a paradigm, and mention some initial experiments in using GPT in the concept design process and as a tutor for novices.
Finding structure in software
Daniel Jackson
Keynote, NASA Formal Methods Conference
May 26, 2022
Slides with builds | Slides without builds
Why are some apps so much better than others, and some designers so much more successful? For the last decade or so, I've been trying to answer this question. My approach has been to study hundreds of popular apps, identifying good and bad parts, and then looking for a way to codify this knowledge so that anyone can use it to become a better designer. In this talk, I'll explain some of the key ideas I came up with: (a) concepts: a way to define the experience of using an app in modular terms, and a basis for codifying common patterns, and (b) design moves: some archetypal moves that software designers make to improve their designs.
Everything you wanted to know about software but were afraid to ask
Daniel Jackson
Leading Jewish Minds, MIT
May 12, 2022
Video
| Slides
How did some software become so easy to use? And why is some software still maddeningly confusing? I'll trace some highlights in the history of software design, and tell you about the ideas that help designers make their software more usable, from user interface heuristics to my own work on conceptual design. I'll explain how many designs today are confusing, either unintentionally or for more insidious reasons.
Concept Design Moves: or how to become a great software designer
Daniel Jackson
Boston ACM/IEEE Chapter
March 24, 2022
Video
| Slides with builds | Slides without builds
Why are some apps so much better than others, and some designers so much more successful? For the last decade or so, I've been trying to answer this question. My approach has been to study hundreds of popular apps, identifying good and bad parts, and then looking for a way to codify this knowledge so that anyone can use it to become a better designer. In this talk, I'll explain what I came up with: (1) a way to structure the functionality of an app into "concepts" (which are essentially little behavioral protocols); (2) a composition strategy that lets you put concepts together without coupling them; (3) criteria for good and bad concept design; and (4) the beginnings of a catalog of reusable concepts. Most of the examples and ideas will be drawn from my recently published book, Essence of Software.
The Essence of Software (Or Why Systems Often Fail by Design, and How to Fix Them)
Daniel Jackson
ACM Tech Talk
Dec 1, 2021
Video | Slides
We've made great strides in software, but many systems are still hard to use or behave badly. Traditionally, we've looked to bugs in code to explain why systems go wrong - or to flaws in the user interface that may lead to misuse. In this talk, I'll argue that the real problem often lies elsewhere: in the very concepts of the design. I'll present a variety of surprising snags with familiar applications, from Dropbox to Gmail, and I'll show how concepts can diagnose them and suggest fixes. I'll explain in concrete and actionable terms what concepts are - essentially free-standing "nano services" that factor the behavior of a system into independent and reusable parts - and how you can apply them in your work, whether you're a coder, program manager, software architect, UX designer or consultant. This talk is based on the book Essence of Software: Why Concepts Matter for Great Design, published by Princeton University Press in November 2021.
Design by Concept: A New Way to Think About Software
Daniel Jackson
EROSS Summer School
Aug 5, 2020
Video | Slides
A New Abstraction for Software Design
Daniel Jackson
Distinguished Lecture, Dept. of Computer Sciences, Princeton University
March 2, 2020
Slides
The internal design of software -- how the code is structured -- is powered by familiar abstractions (such as abstract types, classes and modules). But the external design -- how the software actually behaves -- is usually viewed informally, without the guidance of robust abstractions.
For the last few years, I have been exploring a new abstraction that can shape how we think about software applications and systems, and that provides a way to organize behaviors, encapsulate reusable ideas, and evaluate designs.
In this talk, I'll define this abstraction and show how it can be used to explain a variety of flaws in familiar applications. I'll also present some general principles that attempt to capture some key aspects of good software design.
Compared to previous talks about conceptual design: More substantive treatment of semantics and composition; new Google Drive example.
Certified Control: A Safety Architecture for Self-Driving Cars
Daniel Jackson
Joint work with Nikos Arechiga, Jeff Chow, Jonathan DeCastro, Uriel Guajardo, Soonho Kong,
Dimitris Koutentakis, Angela Leong, Geoffrey Litt, Valerie Richmond, Armando Solar-Lezama, Mike Wang & Xin Zhang
Annual Presentation, CSAIL/Toyota Collaboration
December 5, 2019
Slides
Overview of an architecture we've developed for improving the safety of self driving cars. The key idea is to incorporate an interlock, or safety controller, that can intervene if the main controller misbehaves. But in contrast to traditional interlocks, our interlock does not perform its own perceptual analysis, and has no direct connection to the sensors. Rather, the controller constructs a certificate that offers evidence that the proposed action is safe, along with select (and authenticated) sensor readings in support of that claim. This approach allows the use of sophisticated deep learning methods for perception, while mitigating the risks of them failing unpredictably.
A principled approach to software design
Daniel Jackson
Ninth Summer School on Formal Techniques
Menlo College, CA
May 19-24, 2019
Slides, no builds | Slides, builds
Design is about shaping things to fulfill a purpose; engineering is about making them efficient and robust. Software engineering (aka programming) has advanced in large part because we found principles that make good outcomes more likely. For example, if you apply the principles of representation independence, small interfaces and information hiding, you'll be able to contain modifications more effectively and thus get more maintainable software.
Software design - which, if the word has its standard meaning, is about shaping the behavior of software so that it meets its intended purpose - hasn't yet reached this stage. Today, it's done mostly by trial and error, and the principles that exist are primarily for user interfaces. In these lectures, I'll present a new way to think about software design based on a structure that I call a concept, and will show how a collection of simple principles can explain a variety of design failures in familiar software products.apps from a library of concepts; origins of my work in formal methods, HCI and design.
A new modularity for software
Daniel Jackson
Keynote, OOPSLA/SPLASH 2018 (Boston)
November 7, 2018
Slides, no builds | Slides, with builds
Video
A summary of my work to date on software design with concepts. An overview of what concepts are and how they differ from traditional notions; the role that concepts play in characterizing apps and application families; examples of usability problems and their origins in conceptual design; design rules for concepts, including singularity, uniformity, integrity and genericity; the Deja Vu platform and how it supports codeless construction of apps from a library of concepts; origins of my work in formal methods, HCI and design.
A new way to think about specifications
Daniel Jackson
Keynote, ABZ 2017 (Southampton, UK)
June 7, 2018
Slides, no builds | Slides, with builds
This talk starts by noting a pernicious effect of the otherwise valuable separation of concerns between correctness and pleasantness (in Dijkstra's terminology) or verification and validation (in software engineering lingo): a devaluing of design in software development. It gives examples showing that correctness does not imply usability, safety or security, and argues for software design -- the shaping of the behavioral specification -- as a central activity.
Following this, the talk presents my most recent understanding of concepts and the role they play in design, and three rules for designing and combining concepts: singularity (that each concept has exactly one purpose); uniformity (that a concept's operational principle is context-independent) and integrity (that concepts should be composed conjunctively, preserving their properties).
The Alloyed Joys of Software Engineering Research
Daniel Jackson
Keynote, ICSE 2017 (Buenos Aires)
May 26, 2017
Slides, no builds | with builds
An Alloy retrospective: what Alloy is; how Alloy came about; what Alloy's key ideas are; how well the ideas turned out in practice; what extensions and tools others have built on Alloy; some of my favorite Alloy applications; some lessons I learned from the experience; and a few controversial comments about current directions in software engineering research.
Low Code, Citizen Development and New Programming Paradigms
Daniel Jackson
Accenture, West Technology Practice (San Francisco)
May 8, 2017
No builds
With builds
A review of the state of the art in low-code development platforms: how we got here, what these platforms offer, what some of their limitations are, and a brief summary of two research projects aiming to provide fundamental new language constructs as the basis for future platforms.
The Limits of Verification
Daniel Jackson and Mandana Vaziri
Keynote
Foundations of Software Engineering
November 17, 2016
Slides
Some problems with verification, focusing on the limitations of the idea itself.
Towards a Theory of Software Design
Daniel Jackson
Distinguished Lecture Series
Department of Computer Science
University of Illinois Urbana Champaign
November 7, 2016
Slides
A summary of the state of my work on concepts and software design. New material: critique of the conventional view of the "software problem" in which requirements are treated as behavioral constraints; conceptual analysis of Dropbox problems; clearer articulation of how concepts are defined in terms of their parts. To make room for this new material, most of the examples of concept criteria violations have been taken out, and can be viewed in earlier presentations (such as this one).
Software Design and Why It Matters
Daniel Jackson
Politecnico di Milano, Milan; Paris Mines Tech, Paris; Accenture Paris, Milan and Frankfurt
May 16-20, 2016
Slides with animations,
without animations.
How user-centered design became essential for software; what design thinking is about; and how design thinking can be applied to software. In short (and perhaps not easy to extract from the slides): software is an ideal target for design thinking, but presents two challenges. The first is decomposing the software into units that can be designed largely independently; the second is finding a constructive approach to the convergent phase of design. These challenges are addressed by using concepts/purposes as the unit of design, and by using focused abstract data modeling to explore a concept's design. Well established usability heuristics are a practical way to bring greater user-centeredness to software.
Thank you to Accenture for sponsoring this trip, especially to Tish Miller (MIT), Stephan Brandenburg (London), Avril Braganza (India), Arianna Cantoni (Milan), Noemie Sayada (Paris) and Anna Kibler (Frankfurt) for helping with arrangements; and to Frank Mang (Frankfurt), Gianluca Secondi and Marco Sampietro (Milan), and Marc Bousquet (Paris) for hosting me.
Rethinking Software Design
Daniel Jackson
Keynote, SATURN 2016
May 4, 2016
Design@Large Seminar, UCSD
May 4, 2016
Slides with animations,
without animations.
Video of talk.
Latest version of design theory, with a more pragmatic spin; also some new slides on design vs engineering in the context of software.
What are the Elements of Software Design?
Daniel Jackson
Northwestern University
Chicago, IL
February 29, 2016
Slides with animations,
without animations
An overview of our theory of conceptual design, with new material on efficiency in design (when a single concept can legitimately satisfy multiple purposes)
Towards a Theory of Conceptual Design for Software
Daniel Jackson
Onward! SPLASH
Pittsburgh, PA
October 29, 2015
Slides
An overview of our evolving theory of conceptual design.
A New Approach to Software Design Analysis
Daniel Jackson
Keynote, International Symposium on Software Testing and Analysis
Baltimore, MD
July 2015
Slides
Includes a fuller articulation of the operational principle and its role, and a discussion about the limitations of formal methods applied to conceptual design.
Conceptual Design of Software
Daniel Jackson
Hack Learning: CSAIL/Accenture Design Hackathon
January 2015
Slides
An abbreviated version of earlier talks, aimed at student teams working on a design. Also sets some context in terms of design thinking.
Beyond Design Thinking
Daniel Jackson
Singapore University of Technology and Design
January 2015
Slides
Latest full version of conceptual design ideas.
Conceptual Design of Software
Daniel Jackson
Northeastern University
December 2014
Slides
Conceptual Design: The Essence of Software
Daniel Jackson
Accenture India (Bangalore, Pune, Mumbai)
RVCE and PES Universities, Bangalore
March 2014
Slides with animations,
without animations
(Re)thinking Software Design
Daniel Jackson
Sackler Lecture, Tel Aviv University
December 18, 2013
Slides with animations,
without animations
What is the essence of software design? Researchers and practitioners have for many years quoted Fred Brooks's assertions that "conceptual integrity is the most important consideration in system design" and is "central to product quality". But what exactly is conceptual integrity? In this talk, I'll report on progress in a new research project that explores this question by attempting to develop a theory of conceptual design.
(Re)thinking Software Design By Analyzing State
Daniel Jackson
Workshop Honoring Shmuel Katz, Technion, Haifa
December 19, 2013
Slides with animations,
without animations
Building Systems with Ideas
Daniel Jackson
Accenture, Chicago
April 19, 2013
Slides with animations,
without animations
What's Wrong With Git?
Daniel Jackson
IFIP Working Group 2.3, Kirkland, WA
July 16, 2012
Slides
Conceptual Models in Software Design
Daniel Jackson
Google, Cambridge, MA
May 8, 2012
Slides
I'll argue that the key determinant of the success of a software project is whether or not it's built with robust concepts (and whether those concepts are a good match to the problem). Using a variety of examples, I'll illustrate this claim, and will show a simple way to articulate concepts and their relationships. Then I'll explain how, using the Alloy Analyzer, you can find subtle flaws in conceptual models, and will illustrate this was some recent Alloy case studies done by others, including an application to web security.
Three Applications of Model Finding to Software Engineering
Daniel Jackson
Tel Aviv University, Dept. of Computer Science
March 7, 2012
Slides
I'll tell you about three research projects my group is engaged in, all of which involve the application of model finding to software engineering problems. The first is declarative programming: augmenting a traditional program interpreter with the ability to "execute" declarative specifications, essentially allowing a form of runtime assertion in which the assertion isn't checked, but rather is made to hold by adjusting the program state to satisfy. The second is verifying web applications; we're building a tool that checks Ruby on Rails applications by translating action methods into constraints which are then solved to find counterexamples to specifications. The third is diagnosis of system configurations for security properties, in which information about a system's configuration is combined with desired security properties to obtain evidence of possible attacks, explanations of vulnerabilities, and suggestions of fixes.
How to Prevent Disasters
Daniel Jackson
Keynote lecture
Siren-NL
Veldhoven, Netherlands, November 2, 2010
Slides; Models; Comments on Leveson's example; Blog post by Peter Ladkin on our discussion of the example.
A Structure for Dependability Cases
Daniel Jackson and Eunsuk Kang
Keynote lecture
Abstract State Machines, Alloy, B and Z
Orford, Quebec, February 24, 2010
Slides; Models
A Decade of Alloy: Ideas, Applications, and New Directions
Daniel Jackson
Distinguished Lecture Series in Programming Languages & Software Engineering
University of Wisconsin - Madison
Madison, Wisconsin, November 4, 2009
Slides; Models
Dependences & Dependability
Daniel Jackson
IBM Research, Watson Research Center
Hawthorne, NY, June 1, 2009
Slides
Hoare on JSP
Daniel Jackson
Software Requirements and Design: A Tribute to Michael Jackson
Vancouver, Canada, May 19, 2009
Slides
Hazards of Verification
Daniel Jackson
Keynote, Haifa Verification Conference
Haifa, Israel, October 27, 2008
Slides; Slides with citations (PDF)
Increasing Modelling Confidence With Unsat Core
Daniel Jackson
Invited talk, SPIN Workshop
Los Angeles, CA, August 12, 2008
Slides (PDF)
Why is software so hard, and what can we do about it?
Daniel Jackson
India Delivery Center, Accenture
Bangalore, India, November 29, 2007
Slides (PDF)
An Advanced Introduction to Alloy
Daniel Jackson
Automated Software Engineering
Atlanta, Georgia, Nov 8, 2007
Slides (PDF); Models
Recent Advances in Alloy
Daniel Jackson
Invited talk, Integrated Formal Methods (IFM 2007)
Oxford, July 4, 2007
Slides (PDF)
Software for Dependable Systems:
Sufficient Evidence?
Daniel Jackson
Early briefing of a National Academies Study
National Security Agency, High Confidence Software and Systems Conference
Baltimore, MD, May 9, 2007
Slides (PDF)
Idioms of Logical Modelling
Daniel Jackson
Joint Keynote, ICGT and
SBMF
September 20, 2006; Natal, Brazil
Slides (PDF); Models
Most modeling languages embody a particular idiom: the state/invariant/operations idiom for VDM and Z; the variable-update/temporal-logic idiom for SMV and Murphi; the imperative-programming idiom for Promela and Zing; and so on. Fixing an idiom makes tools easier to build, and helps novice modellers. But it also makes the language less flexible.
Alloy is a modelling language that was designed, in contrast, to support multiple idioms. Its core is a simple but expressive relational logic, whose semantics consists of a set of bindings of relations to global variables. In other words, an Alloy model is a constraint, and its meaning is a set of graphs with labelled edges of varying arity. The Alloy Analyzer is a constraint solver that can find a graph satisfying a given constraint.
A variety of idioms can be readily expressed in Alloy, and analyzed using the Alloy Analyzer. You can structure the state as a global state variable with multiple components, or follow an object-oriented style, where the state is collection of objects, each with components whose values vary of time. You can express and analyze individual operation executions, using the inductive approach of languages like Z, or introduce traces and check them against linear temporal logic properties. Frame conditions can be written as conventional equalities in each operation, or in the style invented by Reiter.
In my talk, I'll explain the basics of Alloy, show how to express a variety of idioms, and demonstrate them on the hotel locking problem (which is the subject of a comparison of several approaches in an appendix of my book, available here).
Alloy in 90 Minutes
Daniel Jackson
Mini tutorial, Requirements Engineering 2005
September 1, 2005, Paris
PDF (colour slides)
A tutorial overview of Alloy.
Dependable Software: An Oxymoron?
Daniel Jackson
Keynote, Requirements Engineering 2005
August 31, 2005, Paris
PDF (colour slides)
Can software really be made dependable? And if it was, would we be able to recognize it? For the last two years, I've been chairing a study of the National Academy of Sciences on dependable software, and have had the opportunity to hear -- in open, public sessions -- anecdotes and viewpoints that have often surprised me. The conclusions of my committee will not be made public until the final report is out. In this talk, therefore, I'll share some of the things we've heard, and draw some connections to requirements engineering.
Relational Logic for Software Design
Daniel Jackson
Lipari Summer School
July 18-22, 2005
Four lectures (all PDF colour slides):
Introduction
Logic, Language and Analysis
Idioms: Invariants, Operations, Traces
Event Idiom and Environmental Assumptions
Examples here
Modelling and Analyzing Software Abstractions
PDF (colour slides)
Daniel Jackson
Distinguished Speakers in Software Engineering Series
Microsoft Research
March 21, 2005
Some Concerns About Aspects
PDF (colour slides)
Daniel Jackson
Brown/Northeastern Aspects Day
Boston, MA
March 8, 2005
I was asked to present a skeptical view on aspect-oriented programming. The first challenge in pursuing separation of concerns is to decide what the concerns are that should be separated. Citing work in viewpoints, views and problem frames, I argue that the fundamental concerns come from the problem domain; describing a concern as 'cross cutting', in contrast, usually just recognizes a deficiency of the chosen implementation structure. Separation of concerns must be maintained in the implementation, which means that concerns must be expressible in a modular fashion. Unfortunately, aspects do not have the key modularity properties that are needed.
A Type System for Object Models
PDF (colour slides)
Jonathan Edwards, Daniel Jackson and Emina Torlak
Foundations of Software Engineering
Newport Beach, CA
November 4, 2004
A simple but powerful type system for object models that offers subtypes and ad hoc union types, and a flexible scheme for resolving overloading. There are no casts or type annotations. Type errors are associated with expressions that can be shown to be irrelevant. This type system has been implemented in Alloy 3, and gives improved flexibility over our earlier type system, catches more errors, and allows the language to be given a simpler, untyped semantics.
Rethinking the Role of Software Design
PDF (colour slides)
Daniel Jackson
2004 MIT Information Technology Conference
MIT Office of Professional Education Programs
April 22, 2004
Extreme programming minimizes the role of upfront design, and encourages the use of code as the medium for exploring designs. This talk explains how analyzable models can provide a better medium for design than code, with earlier and more extensive feedback.
Conceptual Models and Modern Software Construction
PDF (colour slides)
Alloy models and visualizations from demo
Daniel Jackson
MIT Technology Novartis IT Excellence Program @ MIT
MIT Office of Professional Education Programs
March 23, 2004
Analyzable Models for Software Design
PDF (colour slides)
Alloy models and visualizations from demo
Daniel Jackson
Distinguished Lecture Series
University of York, England, February 2004
An overview of Alloy and its applications, with an emphasis on the key ideas behind the research program.
Dependences and Dependability
PDF (colour slides)
Daniel Jackson
High Dependability Computing Program
Talk for Annual Review
NASA Ames, June 2003
A brief overview of some new work on dependences. Regarding modules as specification transducers allows a more fine-grained tracking of dependences. Using this idea, we found some serious flaws in the code of a radiotherapy machine.
Alloy: A Logical Modelling Language
PDF (colour slides)
Alloy models and visualizations from demo
Daniel Jackson
Keynote, 3rd International Conference of B and Z Users (ZB2003)
Turku, Finland, 4 June 2003
A tour of Alloy, with an emphasis on the difference between Alloy and Z.
Alloy: An Analyzable Modelling Language
PDF (colour slides, for printing)
PDF (colour slides, animated)
Alloy models and visualization
Daniel Jackson
Praxis Critical Systems, Bath, UK, April 25, 2003
A whirlwind tour of Alloy for an audience familiar with formal methods such as Z. In one small example illustrates basic semantics, simulation and checking, operation- and trace-based analyses.
Declarative Modelling and Analysis with Alloy
Introduction [PDF, animated]
[PDF, for printing]
Logic [PDF, animated]
[PDF, for printing]
Language [PDF, animated]
[PDF, for printing]
Analysis [PDF, animated]
[PDF, for printing]
Bakery [PDF, animated]
[PDF, for printing]
Elevator [PDF, animated]
[PDF, for printing]
Daniel Jackson
Marktoberdorf Summer School, July 2002
A series of four and a half lectures on Alloy, aimed at students with an interest in a mathematical approach to modelling. No background required beyond elementary logic. The elevator case study was replaced by the bakery example at the last minute (since it had been discussed by John Rushby in his lectures). In that example, the modelling of a procss in the critical section as holding no ticket is bogus and has to be fixed (but the general structure of the model, and the trace-based analysis still holds.)
Micromodels of Software
PDF (colour slides)
Alloy models and visualization
Daniel Jackson
Distinguished Lecture Series, Michigan State University, November 2001.
Overview of the Alloy approach to modelling for a general computer science audience.
Analyzing Objects
PDF (colour slides)
Alloy models and visualization files
Daniel Jackson (joint work with Mandana Vaziri and Allison Waingold)
Workshop on New Directions in Software Technology, St. John, US Virgin Islands, December 2001
Preliminary work. Shows how to construct a simple logical model of Java views. Illustrated on a procedure that manipulates iterators and lists.
A Micromodularity Mechanism
PDF (colour slides)
Alloy model
Daniel Jackson, Ilya Shlyakhter, Manu Sridharan
ACM SIGSOFT Conf. Foundations of Software Engineering/European Software Engineering Conference (FSE/ESEC '01), Vienna, September 2001.
Describes new version of Alloy, focusing on the fundamental idea of the signature. Illustrated on a small railway example. The paper contains many details not covered, including polymorphism, signature extension and a demonstration of the use of the mechanism in a variety of idioms.
Lightweight Formalism
PDF (colour slides),
PDF (black on white, two/page)
Daniel Jackson, MIT
NASA Ames, August 14, 2001
Overview of Alloy approach to the use of models in software development. Illustrates application of Alloy at both abstract design and code design levels to a text tagging program.
Lightweight Formal Methods
(PDF)
Daniel Jackson, MIT
Keynote Lecture, Formal Methods Europe, Berlin, March 14, 2001
Formal methods have offered great benefits, but often at a heavy price. For everyday software development, in which the pressures of the market don't allow full-scale formal methods to be applied, a more lightweight approach is called for. I'll outline an approach that is designed to provide immediate benefit at relatively low cost. Its elements are a small and succinct modelling language, and a fully automatic analysis scheme that can perform simulations and find errors. I'll describe some recent case studies using this approach, involving naming schemes, architectural styles, and protocols for networks with changing topologies. I'll make some controversial claims about this approach and its relationship to UML and traditional formal specification approaches, and I'll barbeque some sacred cows, such as the belief that executability compromises abstraction.
Includes sneak preview of new version of Alloy, with structuring mechanism and arbitrary-arity relations.
Alloy Revisited
(PDF)
Daniel Jackson, MIT
IFIP Working Group 2.9 on Requirements Engineering
Hawk's Cay, Florida
February 19, 2001
A new version of Alloy with structuring. BART example revisited. Why declarative style is important.
Logic, Models and Analysis
Daniel Jackson, MIT
Invited Lecture
7th International Static Analysis Symposium
Santa Barbara, CA
June 29, 2000
Overview of Alloy and its analyzer, with sample applications to models and code.
Unintentional Naming
Daniel Jackson, MIT
Lab for Computer Science Annual Retreat
June 26, 2000
A brief talk describing Sarfraz Khurshid's case study of Intentional Naming using Alloy.
Future of Software Analysis
Daniel Jackson, MIT
Future of Software Engineering Track
International Conference on Software Engineering
Limerick, Ireland
May 2000
Based on a paper with Martin Rinard.
A Relational Logic, Its Analysis and Application
Part A / Part
B
Daniel Jackson, MIT
IFIP Working Group 2.3 on Programming Methodology
Newcastle, England
April 4, 2000
Part A gives an outline of the Alloy modelling language and shows how it was used in an analysis of Microsoft COM (joint work with Kevin Sullivan). Part B describes the analysis of Alloy by translation to SAT, and includes brief comments on a new symmetry breaking scheme developed by Ilya Shlyakhter.
Shape Analysis with SAT
Daniel Jackson, MIT
Workshop on Model Checking & Program Analysis
Schloss Ringberg
February 21, 2000
Joint work with Mandana Vaziri
I presented a new method for finding bugs in code using SAT. The code of a procedure is translated into an Alloy formula. A second formula is obtained by combining this formula with a user-defined specification, whose models are executions of the procedure that violate the spec. The Alcoa checker is then used to find models. I illustrated the use of this method to find shape analysis bugs in a benchmark suite of programs used previously by Sagiv et al. The method is not sound, since it may miss bugs, but is complete (so long as datatypes aren't abstracted). The merit of the approach is its ability to handle user-defined specs, not only to check code against, but also as surrogates for called procedures.
Tractable Object Modelling
Daniel Jackson, MIT
IFIP WG 2.9, Flims, Switzerland
February 7, 2000
I explained the motivation behind lightweight formal methods, and presented Alloy, a new lightweight object modelling language. I illustrated the simplicity of aspect by showing how it treats partial functions. I showed how to use Alloy and its automatic analyzer Alcoa to investigate the placement of gates in the BART system, and to check that a gate policy has the intended safety consequences. Finally, I explained why the problem of analyzing Alloy models is hard -- often involving the consideration of 10^100 states -- but in practice usually possible in seconds.
Back to Daniel Jackson's home page