I’ve been using Alloy for well over a decade now, but I’m looking to get more out of it (inspired by a research arc spanning from Jackson’s “A direct path to dependable software” to Torlak’s “How We Built Cedar: A Verification-Guided Approach”). There have only been a few occasions where I used Alloy in a team setting (where the model(s) were maintained alongside the system, kept in version control, and served multiple purposes throughout the software development lifecycle); I mostly use Alloy to explore and understand a design space, having the computer amplify and accelerate my understanding, and to identify the critical invariants within some design – purely a personal tool.
I’m now very interested to see Alloy deliver value throughout the entire SDLC, organizing dependability cases, and collecting evidence from multiple subsystems into one model that is run as part of a standard continuous integration pipeline. We can see a similar approach taken in Daniel Jackson’s proton therapy work, as well as Emina’s “Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers,” and analogous approaches with different tooling from the lightweight formal methods approach detailed in the AWS S3 work (" Using lightweight formal methods to validate a key-value storage node in Amazon S3") and the later Cedar work mentioned above.
With that in mind:
Are there any practitioners here that use Alloy in this fashion that can share a brief field report about what has been successful and pitfalls to avoid?
Is there interest in the Alloy community to see the evidence extension added permanently to Alloy, enabling the use of external tools/checkers to establish properties within an Alloy model?
Slightly unrelated, has anyone taken traces from Alloy 6 and visualized them with ShiViz? Is there any interest in seeing a ShiViz-like view within the standard visualizer? The motivation for this last one relates to Alloy models expressed in Markdown, with ShiViz JSON traces as component of the documentation for a system.
My teams currently use a lightweight formal methods approach quite similar to what’s described in the S3 paper. I think this is becoming more common in industry with the growth in “always on; never fail” systems - five-nines or better with significant liability clauses. Cedar’s “Verification-guided approach” is an evolution of the same idea.
My interest is in how an initial effort made a requirements/design time can deliver value throughout the entire SDLC, across iterations, across tooling, and continue to evolve with the project. Similar goals can be seen by those in safety engineering (Nancy Leveson has had some wonderful pieces in ACM Communications the past few years and I share her views).
Finally- many, many thanks to everyone involved with Alloy, including all the wonderful labs around the world doing interesting things with Alloy. You might not hear it often, but your works matters a lot to some us industry, and we spend some of our lunches discussing your works and imagining how we’d do things differently if your work was part of Alloy mainline.
ShiViz looks interesting. I don’t know of any such work in the context of Alloy but it looks like it wouldn’t be too hard to devise regexps for Shiviz to parse an Alloy model. Notice that in the soon-to-be-released next version of Alloy, thanks to @peter.kriens, it will be possible to output instances in the terminal (incl. with a JSON format), thus easing post-processing with other tools.
Hi,
Thanks for the reply! That’s great news about the outputting instances with JSON. P does a similar approach within the VS Code tooling – exporting instances/traces in a well-documented text format, and post-processing it for use in other tools (including ShiViz). I’ll build the latest code and give it a try, thank you.
The evidence extension is described in Emina Torlak’s paper, “Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers.” ( 2016, https://homes.cs.washington.edu/~mernst/pubs/neutrons-cav2016.pdf ). Section 4 describes the extension as an “evidence predicate” which enables Alloy to have bridges into other tools, collecting the results within the Alloy model (the “Safety Case Checker”). It’s possible to implement something similar/limited as a pre-processor of the Alloy model which generates a final model to pass back into the Analyzer.
An example from the paper to provide a sense of how it looks (Fig. 2):
1 evidence [ PLC_Analysis ,
2 " -- mode " -> " all - paths - to - coil - contain - relay " +
3 " -- network - file " -> " plc - code / cyclotron / mod1 . stu " +
4 " -- coil " -> " % M1623 " +
5 " -- relay " -> " % M2754 " ,
6 Proof ] = >
7 all relayOpen : Relay2754 . state & RelayOpen |
8 some coilState : Coil1623 . state & CoilDeenergized ,
9 coilChangeSignal : PLC . sentMsgs & CoilChange |
10 coilState in relayOpen . next and
11 coilChangeSignal in coilState . next and
12 coilChangeSignal . coil = Coil1623 and
13 coilChangeSignal . state = coilState
Description from the paper:
The language is extended with a small library that provides the uninterpreted
evidence predicate. In particular, the formula evidence[tool, args, kind] represents
the presence (or absence) of the given kind of evidence, produced by invoking
the specified tool on the provided arguments. The checker, as shown in Figure 4,
provides an interpretation for each evidence predicate in a safety case by performing
the specified tool invocation and recording the result in Alloy. This invocation
is performed through a simple plug-in interface, designed for easy addition of
new tools to the checker. The resulting interpretation I gives meaning only to
the evidence predicates, and, as such, it is a partial interpretation [ 44, 47] for the
safety case S ⇒ P , which includes additional relations (e.g., the next relation in
Figure 2). The checker passes I and S ∧ ¬P to the Alloy Analyzer, which checks
that I cannot be extended into a finite counterexample to the safety case—i.e.,
an interpretation I′ ⊇ I that satisfies S ∧ ¬P in a finite universe of discourse.
The results of SCC verification are sound up to the bound on the universe size,
modulo any bugs in the implementation of SCC and the pluggable checkers.