User Tools
Sidebar
This is an old revision of the document!
Table of Contents
Eiffel: the Method
Eiffel is an industrial strength object-oriented language that has influenced other languages such as Java, C# and UML. It is a pure, statically typed OO language, and is used for complex systems where it provides the right paradigms to address the construction of large, high-quality object oriented software systems. Eiffel is more than a language; it is a framework for thinking about, specifying, designing and implementing object-oriented software. It has built-in support for Design By Contract (DbC) that supports the use of specification and validation of designs as part of foundational computational thinking. Students who learn the benefits of principled thinking and see the value of the related tools will retain these lessons throughout their careers.
PVS
PVS (Prototype Verification System) is a specification language and theorem prover for validating specifications. PVS helps engineers to design coherent specifications, and to predict the behaviour of systems satisfying the specifications — before implementing them. PVS provides interactive assistance to prove theorems that validate the specifications/models. PVS has been used by OPG to certify nuclear reactors, by NASA for space/avionic systems, and in a large number of other mission critical applications. PVS is both a language and an inference system. The language is a typed higher order logic, featuring undecidable type checking. You cannot write code (such as Java, Ruby or Haskell). You can only write mathematics. It thus forces one to write specifications of systems (i.e. what systems do free of implementation detail) and not how they do it. Furthermore, PVS can so some automatic syntax, typing and other checks that helps ensure that specifications are meaningful. PVS can then be used to validate the specifications. PVS was featured in the movie The Martian.
TLA+
TLA stands for the Temporal Logic of Actions. TLA+ is the TLA specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems.
PlusCal is an algorithm language that, at first glance, looks like a typical tiny toy programming language. However, a PlusCal expression can be any TLA+ expression, which means anything that can be expressed with mathematics. This makes PlusCal much more expressive than any (real or toy) programming language. A PlusCal algorithm is translated into a TLA+ specification, to which the TLA+ tools can be applied.
The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+ proof system. All the tools are normally used from the Toolbox, an IDE (integrated development environment). Go to the TLA home page to find out more about TLA.
TLC is a so-called “explicit-state” model checker that computes the state space generated by your specification and can then verify (safety and liveness) properties fully automatically. Its main constraint is state space explosion: the size of the state space grows exponentially with the number of processes etc., and this leads to a corresponding increase in verification time. There are a number of techniques to push back the frontiers of what TLC can handle effectively, including using symbolic constants, symmetry reduction etc., but the most important one is for you to decide how big you need your model to be to have enough confidence in correctness.
TLAPS is an interactive proof assistant: you provide a proof of why your system satisfies a property, and TLAPS can check if that proof is logically consistent and complete. It uses different automatic back-ends, including SMT solvers, to check proof steps, but it is still the user who designs and writes the proof. Although the effort is independent of the size of the state space, and also infinite-state systems can be verified in this way, I would not recommend using TLAPS for users who do not have sufficient experience with theorem proving.
