Daniel Jackson: Recent Talks


The Limits of Verification
Daniel Jackson and Mandana Vaziri
Keynote
Foundations of Software Engineering
November 17, 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).


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