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