Effectively Using JML
Software Engineering Processes incorporating Formal Specification
Using a formal methodology, like that embodied by JML, for software construction is more than learning a specification language, a set of tools, and hiring some experts---it also means successfully applying the ideas, tools, and techniques in a coherent way to the *process* of software construction. Typically, this process is realizing in one of two extremes, what I call "Contract the Design" (annotating software you did not write) or "Design by Contract" (annotating software you are writing). This talk will discuss the core facets of a successful JML-centric software process at these two extremes. A case study embodying these facets, an Internet voting tally/counting application developed with JML for the Dutch government, will also be discussed.
Software engineering with formal methods is difficult but can be very rewarding. Using the basic features of tools like ESC/Java2 is quite easy, but as soon as moderately complex verification is attempted, a deeper understanding of the tool and its underlying theory and architecture is necessary. This talk will discuss the architecture of ESC/Java2, how to incorporate ESC/Java2 into a verification-centric software development process, and how to manage specification and program code complexity. This talk also discusses some of the standard hints and tricks used in program specification to deal with typical verification challenges.
Using Formal Methods for VLSI Development
Using Java and JML in the Real World
Formal methods have been successfully used in non-software industries for many years, most notably in VLSI design firms like Intel, Sun, Hewlett-Packard, SGI, Motorola, and IBM. Recently, some firms have begun to use Java for CAD tool development, primarily because existing tools were inappropriate for new technologies like asynchronous VLSI (AVLSI). This talk will discussed the adoption of Java and JML at the leading AVLSI firm Fulcrum Microsystems. In particular, it discusses what AVLSI is, and how and why Java and JML were incorporated into Fulcrum's software engineering process.
Models are the `M' in JML
Using ADT Models in Formal Specification with JML
Writing complex abstract specifications in JML means writing model-based specifications. Models are mathematical abstractions like sets, lists, and relations that are used to specify abstract behavior in software systems. JML models are realized in a suite of a few dozen functional, ADT-based, richly specified, executable Java classes. This talk will discuss OO/ADT-based models, how JML realizes those models, how models are designed and implemented, and how to use models in specification, testing, and verification.
The ESC/Java2 Calculi and Object Logics:
Implications on Specification and Verification
ESC/Java2 is an extended static checker for Java. It can automatically, modularly verify that some Java programs conform to formal specifications written in the Java Modeling Language, a behavioral interface specification language for Java. This talk will discuss JML and ESC/Java2, and pay particular attention to how ESC/Java2's (a) program calculus for generating verification conditions and (b) object logic for specifying Java semantics play key roles in the specification and verification of real-world, non-trivial Java software. Software engineers interested in formal program development, theorem prover users and developers, and programming language semantics and verification researchers will find this talk particularly illuminating.