This message consists of four parts that may be of some interest to your Helsinki deliberations. While the paper and report described below do not particularly focus on education, they may suggest areas within which to focus educational activities. Our Z/EVES system has been extensively used for teaching purposes. I have attached a brief description of our upcoming release and then some comments from educators in the US, UK and NZ.
Overall, Z/EVES appears to being used in a lightweight perspective
for teaching. Few students/lecturers move through the adoption
curve to performing complex proofs. Obviously, time and experience
is an issue. However, there have been a number of undergraduate
and graduate projects that have used the full capabilities of
the system (with varying degrees of success). Various researchers
and commercial types have pushed Z/EVES to its full extent.
The objective of this study is to identify factors leading to the success or failure of the application of formal methods as exemplified by their use by industry and through past R&D programmes. The objective has been achieved through the review of existing surveys, the review of programme evaluations, and interviews with formal methods practitioners, sponsors and other (past or present) technology stakeholders.
The application of formal methods has a long history but they have not been substantially adopted by the software engineering community at large and we have identified numerous reasons for the failure to adopt. However there is a significant take up of formal methods in critical industries. Large hardware vendors are either developing in-house capabilities in formal verification (e.g. Intel, Siemens) or are adopting externally developed technologies and in the area of safety there is active research, case studies and serious application of formal methods throughout the safety lifecycle. We calculate that about $1-1.5B is spent annually on formal methods activities world-wide.
We identify factors to increase the adoption of formal methods. One major recommendation is that unlike other R&D programmes we have investigated, the strategy of any future investment programme should adopt the Moore Technology Adoption Life Cycle (TALC) "chasm crossing" approach and take a more explicit view of how the market in high technology products actually develops. We consider this to be the single most likely factor to increase the chance of successful adoption. We also identify the need for sustained investment in tools and continued R&D.
AVAILABILITY: Should be available from www.adelard.co.uk
sometime on June 25th. If it's not there in a few days, let me
know and I'll distribute copies of the report to interested parties.
(A paper will also be published as part of the SAFECOMP proceedings.)
Drawing from the author's twenty years of experience in formal methods research and development, and, particularly, with the EVES-based systems, this paper provides personal impressions on what is and what is not working with regards to the adoption and application of formal methods.
As both the community's understanding of technology transfer issues and formal methods technology improve, one is optimistic that formal methods will play an increasingly important role in industry. However, significant impediments continue to exist with, perhaps, the increasing complexity of systems being both a blessing and a curse.
AVAILABILITY: This paper is available from Springer at http://link.springer.de/link/service/series/0558/bibs/1680/16800077.htm.
The last public release of Z/EVES was version 1.5. Several significant improvements were made between versions 1.5 and 2.0 of Z/EVES, including:
Z/EVES uses state-of-the-art formal methods techniques from Europe and North America, integrating a leading specification notation with a leading automated deduction capability. The resulting system supports the analysis of Z specifications in several ways:
Z/EVES supports almost the entire Z notation; only the unique existence quantifier in schema expressions is not yet supported. The Z/EVES prover provides powerful automated support (e.g., heuristics and conditional rewriting) with user commands for directing the prover (e.g., instantiate a specific variable or introduce a lemma). We have automated much of the Z Mathematical Toolkit and included this extended version with the Z/EVES release.
Interaction with the Z/EVES system can occur in three different ways:
Z/EVES runs on SunOS, OS/2, Linux, Windows'95/'98/NT and, with the appropriate compatibility package from Sun, Solaris.
Z/EVES has already been used on reasonably large specifications for type checking, schema expansion and domain analysis. These examples have led to plans for commercial use of Z/EVES. As well, Z/EVES has been used to teach Z and theorem proving.
More information is available on our Web pages, at http://www.ora.on.ca.
AVAILABILITY: The new version of Z/EVES should be available
by late June 2000.
Here at the University of Waikato, we have been using Z/EVES in our 4th year `formal software engineering' course for the last two years.
We've used the Linux version, running under Emacs. Students use it for type checking, testing schemas against example data (both positive and negative), animation (that is, forward execution), and a small amount of precondition calculation and schema simplification. We do not teach proof techniques (other than 'prove by reduce'!).
Students generally find it quite useful and usable, though some complain about the LaTeX notation. We have not tried the new version with GUI yet, but will probably do that this coming semester.
I think the good aspect of using Z/EVES is that it gives students something to interact with -- something that often says: `this is wrong', and forces them to clarify their ideas. In this role, it fulfills the same purpose as a compiler for a programming language. A bad aspect is that quite often Z/EVES will be unable to simplify something for non-obvious reasons, and it is difficult to know how to teach a mental model for what it can and cannot do. We currently take a "try it and see what happens" attitude.
I have some experiences of using Z/EVES for teaching:
last November, I demo'd various Z tools to students on my MSc 1-week course on Formal Spec. I tend to work on the principle that, in 1 week, it's better to teach Z `by hand' and show what tools are available, so students can go off and learn the tools after the course, rather than being distracted by technology during the course. I demo'd Z/EVES (1.3), Formaliser and CADiZ. Easily the most popular was Formaliser, perhaps because you could easily link it with Word? I think the interface was what let Z/EVES down then. (Specially annoying because I'd seen the GUI at FM'99!) Our students don't know LaTeX, so there's an awful lot to learn before (the old) Z/EVES is usable.
In March, I showed Z/EVES 2.0 and CADiZ on a Refinement and Proof course. This time, Z/EVES won hands down! Vastly improved interface, good documentation. On the down side was the difficulty of linking with something like Word, the confusion of having to enter `keywords' like seq, dom and ran in a special way rather than through the standard keyboard, and (for me at least) the diffculty of seeing where I was in a proof (eg, in a proof by cases, I have been known to forget that there's another case to do and therefore be surprised by getting to `true' and not having a finished proof!) This is one place where CADiZ wins. But overall, Z/EVES was certainly popular: I'll be using it again in both courses next academic year.
I have, and continue, to use Z/EVES for the Models of Software Systems course here at CMU.
The version I've used so far has been the non-GUI (1.5) version. The reason for this approach has been that students seem to have more trouble installing software than running it! This is particularly true when companies have policies concerning the amount of software students can install.
Overall, our use has been minimal (I don't ask them to do more than check specifications) however, use has been beneficial. The error messages are, sometimes, cryptic - a problem that is compounded by, in some cases, Z/EVES insisting that every error occurs on line 1. I haven't tracked the cause of this problem down as yet.
One student went further last year and developed some interesting specifications (unfortunately not only the specification but the subject matter contains proprietary information that I cannot pass on). His experience was positive except for the point where he got to performing some significant proofs. Z/EVES was able to perform a number of the simpler proofs but, for the more complex situations, disappeared into never-never land. I suspect that part of the problem is that the student hadn't created his specification in such a way that it was really amenable to proof. A fact that came up late in the process for various reasons.