Specification languages

The ASM Method

The Abstract State Machines (ASM) Method is a systems engineering method that improves current industrial software development practice by using accurate high-level modeling where the descriptions at the successive design stages are linked in an organic and efficiently maintainable chain of rigorous and coherent models at stepwise-refined abstraction levels. It supports the major software life cycle design and analysis activities in a controllable (read: documentable and verifiable) way, leading seamlessly from systems requirements capture through further design to coding and code maintenance. Within a single and simple conceptual framework it covers modeling at any level of abstraction, verification by reasoning techniques, and validation by simulation and testing.

The method is based upon three notions: Gurevich's ASMs (models that come as a semantically accurate form of pseudo-code) and Boerger's concepts of ASM ground models (system blueprints one can show to faithfully capture requirements) and ASM refinements capturing in provably correct ways the stepwise introduction of design decisions that lead from abstract models to their implementation by executable code. Since the 1990'ies the method is used in a number of industrial projects (in particular at IBM, Siemens, Microsoft and SAP) and of standardization efforts (e.g. at ISO, IEEE, ITU, ECMA) as well as in a great variety of research projects on design and analysis (covering both validation and verification) of architectures, languages, compilers, control systems, protocols, web services, etc., see the Historical Survey

Since 1993 regular annual conferences are organized which are devoted to the method: its theory, applications and tools. Information on non-proprietary research material and ASM tool support can be found at the ASM website

The AsmBook (2003) contains an introduction into the method and a survey of the current tool support, namely for ASM validation by interpreters and test generators and for ASM verification by various model checkers and theorem proving systems (e.g. PVS, KIV). ASMs can also be viewed as extension of Finite State Machines by allowing simultaneous reading and updating not only of the three FSM locations internal state, input, output, but of arbitrarily many memory locations containing values of arbitrary type. See ASM Tutorial

Challenges

The overall challenge is to define and to provide tool support for generators of hierarchies of mechanically verifiable ASM refinement patterns, which link in a provably correct way the application-content of systems, as defined by ASM ground models, to to-be-verified compilable programs. It is targeted to encapsulate some specific design experience into the ASM method, turning so to speak part of the design into a language-supported (where possible mechanized) procedure. It implies the necessity to enhance the current tool support for the simulation of ASMs, for the verification of their properties and for linking models at different levels of abstraction. This overall goal splits into a certain number of subgoals formulated in http://qpq.csl.sri.com/vsr/private/theory/boerger-facjverifcompil.pdf/view and transscribed here.

• Refinement Generator The refinement generator challenge consists in generating practical model refinement schemes, which capture established programming knowledge, together with justifications of their correctness. Refinement steps whose generation can be automated are to be expected typically in domain-specific applications. Where the refinement process is highly creative, interactive schemes can still be helpful to guide the refinement process by a combination of user-insight and mechanized tactics.
• Refinement Verifier The refinement verifier challenge consists in enhancing current logical or computer-based verification systems by means to prove the correctness of ASM refinement steps. A concrete example of this challenge is the following challenge.
• Java/JVM and C#/CLR Verification Verify by existing mechanical theorem proving systems the following theorems, proved in the Jbook (2003) using layered ASM models for interpreters of Java and the JVM. 1. Java is type safe (Thm.8.4.1) 2. Correctness of the Java2JVM compilation scheme (Thm.14.1.1) 3. JVM invariants for the soundness of Bytecode Type Assignments (Thm.16.4.1) 4. Completeness of the scheme for certifying Java2JVM compilation (Thm.16.5.1,16.5.2) 5. Soundness of the bytecode verifier (Thm.17.1.1). Part of this challenge consists in providing modular proof schemes that reflect the hierarchy of the layered ASM models for Java/JVM. Reuse the computer-based verification of the JavaCard-without-subroutines subset of Java (see Gerwin Klein and Tobias Nipkow, A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler, TR 0400001T.1, National ICT Australia, 2004 and to appear in ACM TOPLAS and G. Betarte, E. Gimenez, C. Loiseaux, B. Chetali. FORMAVIE: Formal Modelling and Verification of the Java Card 2.1.1 Security Architecture. Proc. eSmart 2002). Reuse the Java/JVM verification proofs to establish the corresponding theorems for C#/.NET CLR, using the corresponding ASM models developed in a series of recent papers. A similar project, mechanically verifying a mathematical proof for the correctness of a compilation scheme from Prolog programs to Warren Abstract Machine (WAM) code starting from an ASM for ISO Prolog and leading through 12 ASM refinement steps to an ASM for the WAM, has been successfully carried out in the 1990'ies using the KIV prover
• Refinement Validator The refinement validator challenge consists in linking the refinement of ASMs to ASM execution tools to make the generation and systematic comparison of corresponding test runs of abstract and refined machines possible. In particular relating system and unit level test results should be supported by this enhancement of ASM execution tools.
• Integration Develop tool support for a combination of ASMs with specific features provided by other theoretically well defined and practically useful specification languages, like B, Event-B, RAISE, CSP, etc.

ACL2

ACL2 is both a programming language in which you can model computer systems and a tool to help prove properties of those models. See the ACL2 home page.

The B Method

The B-Method was orginally developed by Jean-Raymond Abrial. It is a collection of mathematically based techniques for the specification, design, and implementation of software components. See Atelier B and B-Core.

Perfect Developer

Escher Technologies' Perfect Developer a tool for developing correct object-oriented software. Specifications are written in the tool's language, Perfect, and then refined to code. The tool's theorem prover is used to discharge proof obligations.

VDM

The Vienna Development Method is a set of techniques for modelling computing systems, analysing those models, and progressing to detailed design and coding. VDM has its origins in the work of the IBM Vienna Laboratory in the mid-1970s; however, the notations and tools have steadily developed and are now applied on a wide range of systems.

The Z Notation

The Z notation is a specification language based on elementary set theory and logic, and is used for producing structured descriptions of software systems. It was invented by Jean-Raymond Abrial, and further developed by the Programming Research Group at Oxford. The Z User Group organises regular conferences devoted to the language and its tools.

Z was used in the 1980s in a number of industrial projects to assist developers of hardware and software systems. Particularly notable were two industrial collaborations, each of which won Queen's Awards for Technological Achievement. The first was the development of the inmos floating-point transputer, and the second was the specification and development of modules for the IBM CICS transaction processing system. These projects helped to develop the language, and in particular its structuring mechanism, the schema.

The notation was defined formally by Spivey in his book Understanding Z (1988), and this was followed by an informal description and guide to the notation in The Z Notation: A Reference Manual (1989, 2nd edn 1992). A group of industrial users worked with Oxford to produce a definitive standard for the syntax, semantics, and logic of Z, and this resulted in ZIP, a five-year project funded partly by the UK government, and partly by the industrial partners. When ZIP ended, the language definition committee continued its work by developing an ISO international standard, which was published in 2002.

A number of textbooks are available for Z, including The Way of Z and Using Z.

There are several mature tools for Z, including the Z/Eves and ProofPowerZ interactive theorem provers, and the Jaza animator.

Challenges

• Verification

  Z is one of the more popular formal methods: it has shown its suitability for describing large specifications of software systems. Because of its popularity, there are a number of interesting formal specifications available for experimentation. Many of these specifications were written before the proof tools for Z became mature enough to be useful. The Mondex Case Study is a good example of this: the proofs of correctness were carried out by hand ten years ago. The challenge is to see if these can be mechanised today with a high degree of automation.

• Refinement

  There is a well-developed theory of refinement in Z, but few examples of successful formal development of large specifications all the way into code. This is due to the enormous effort that is required to carry out the calculations needed. The challenge is to reduce this effort with appropriate tool support.

• Integration

  Z has proved its usefulness, but so have several other formal specification languages, including Alloy, VDM, Raise, B, CSP, the refinement calculus, and Perfect Developer. The challenge is to combine the best advantages of all these state-based specification and refinement notations, and to get the different communities to work together to use the combination.