VeriTLA

Un article de Loria Wiki.

Sommaire

[modifier]

ARC VeriTLA+ : A Verification Environment for TLA+ Applied to Service Descriptions

VeriTLA+ is a cooperative research initiative funded by INRIA for the years 2006 and 2007. The objective of VeriTLA+ is the development of a verification environment for TLA+ and its application to domain-specific languages for services, including scheduling of tasks in operating systems and telephony services.

The following groups are participating in VeriTLA+

MOSEL contributes to the construction of the proof environment for TLA+. Specifically, work is underway for encoding TLA+ in the interactive proof assistant Isabelle. Moreover, MOSEL is involved in the design and implementation of the SMT solver haRVey, and we work on the integration of interactive and automatic deduction tools, based on proof reconstruction. MOSEL is also interested in formal methods for the design and verification of distributed algorithms through abstraction and refinement.

PHOENIX develops domain-specific languages and supporting analysis tools. In particular, the team has defined DSLs for programming telephony services. Within the VeriTLA+ project, PHOENIX will investigate describing the semantics of these languages in TLA+. By generating TLA+ models from programs implementing telephony services, properties of these programs can be verified using the TLA+ tools.

GALLIUM contributes to the TLA+ proof environment, in particular through the Zenon theorem prover for first-order logic that serves as a workhorse for discharging proof obligations in predicate logic and elementary set theory.

The OBASCO team has developed many domain-specific languages, together with formal semantics and supporting tools. Of particular interest to the project are the Bossa language for which several properties have been proven by static analysis and using FMona, and the Coccinelle language for describing semantic patches to OS drivers.

The ACADIE team is interested in formal methods and proofs for distributed systems. They are investigating static type systems for TLA+, and they have developed FMona and used it for verifying properties of Bossa programs.


Associated partners of VeriTLA+ are

The initial project proposal is available, as are the presentations of the project at the ARC days in Grenoble 2006 and Rennes 2007.

[modifier]

Conclusions

The VeriTLA+ project involved research groups from two distinct communities. The Obasco and Phoenix teams have much experience in the design of domain-specific programming languages (DSLs) and associated tools (for compilation, static analysis, optimization etc). The Acadie, Gallium, and Mosel teams work on methods and techniques for the formal verification of software and systems. Associated partners were Leslie Lamport (Microsoft Research) and Julia Lawall (DIKU Copenhagen). The objectives of the project were to intensify the interactions between the two communities, focusing on work around the TLA+ specification language. More specifically, we set ourselves two goals: contribute to the development of a verification environment for TLA+, and use TLA+ for formalizing the semantics of DSLs and for the subsequent verification of programs.

The project meetings were occasions of interesting discussions between the participants and resulted in punctual cooperations between the partners. Despite encouraging preliminary results, these were not followed up by longer-term actions involving teams from both communities, essentially because of lack of full-time manpower devoted to the project. (Two successive candidates for a post-doctoral position attributed to this project ended up declining the offer, and we were not able to fill the position during the second project year.)

Work carried out in VeriTLA+ can be categorized as follows:

  • Development of a TLA+ proof language and support tools (Gallium, Mosel, MSR): we have contributed to the design of a declarative, hierarchical proof language for TLA+, helping a user to structure a verification project. It is expected that automatic provers discharge proof obligations at the leaf level of the hierarchy, and that the overall correctness of the proof structure is certified by the proof assistant Isabelle, based on proof traces produced by these automatic provers. A first prototype of an interpreter of this language has been developed during an internship project in the summer of 2007, using some advanced functional programming concepts. Members of Gallium and Mosel have continued developing back-end provers (Zenon, haRVey, and Isabelle) for the planned proof environment, adapting them for TLA+ formulas. They have also worked on the generation of proof traces by the automatic provers and their certification by proof assistants.
  • Verification for domain-specific languages (Acadie, Mosel, Obasco, Phoenix, Diku): work mainly concerned (variants of) the call-processing language CPL for the implementation of telephony services and the language Bossa for programming schedulers for operating systems. Previous work had revealed some limits of purely static verification techniques. A translation of CPL into TLA+ models has been defined and implemented within the existing compiler. In this way, default properties (such as the absence of cycles for call forwarding) as well as user-specified properties can be verified with the TLA+ tools. In a similar spirit, Bossa programs are represented as state transition systems, and the correspondence of these programs with abstract scheduling policies for a given operating system can be verified automatically, using the Mona tool.
  • Verification of distributed algorithms: (Acadie, Mosel, MSR): The TLA+ tools were evaluated over a number of classical distributed algorithms such as group membership protocols or distributed consensus. The verification has been performed using either model checking techniques (using the TLC and +CAL tools) or by theorem proving in Isabelle. This has led to an extension of the +CAL language and the perspective of applying model checking techniques for Grid and peer-to-peer programs implemented using the Gras library of SimGrid.

Beyond the immediate cooperations within the project, VeriTLA+ has catalyzed some ongoing joint work by the project partners. In particular, Damien Doligez is becoming involved in the Coccinelle project on semantic patches of Linux drivers.


In conclusion, we are grateful for the possibility of testing new partnerships within the VeriTLA+ project. Unfortunately, the project results are reflected in only a limited number of joint publications, and the tools are still at a prototype stage. On the positive side, the project gave us a forum for interesting discussions, and the tool development will continue outside the project.

[modifier]

Activities

  • TLA+ proof language and proof manager (Gallium, Mosel, MSR)

A hierarchical and declarative language for writing formal proofs in and for TLA+ was designed and the existing parser for TLA+ was extended. The design of the language roughly follows Lamport's paper How to Write a Proof, but adds some derived proof elements that simplify use in actual verification. It is intended to be formally verifiable by the kernel of an interactive proof assistant such as Coq or Isabelle; the leaf proofs can be delegated to automated theorem provers. A first prototype in OCaml (relying on alpha-Caml and Moca) was implemented during the internship of M. Notti in Nancy.

  • Back-end provers for TLA+ (Gallium, Mosel)

Two back-ends exist currently that are to be used within the TLA+ proof environment: Zenon is a tableau-based first-order prover, whereas haRVey is an SMT solver. Both output formal proofs that can be checked by interactive proof assistants. Our work has focused on extending haRVey and Zenon for set-theoretic reasoning; in particular, a new decidability result has been obtained for the Bernays-Schönfinkel-Ramsey class of formulas.

  • Proof generation and certification (Gallium, Mosel)

Zenon exports proofs for Coq as either proof tactics or proof objects. Proof certification has been implemented for propositional logic and for uninterpreted function symbols with quantification for haRVey within Isabelle. This has given rise to interesting problems regarding the efficiency of proof reconstruction. We have used reflection to allow for more efficient proof certification from within Isabelle.

  • Verification of telephony services (Mosel, Phoenix, DIKU)

A compiler for CPL (call processing language) has been implemented that generates a TLA+ model from a CPL/VisuCom program. The TLC model checker has been used to verify domain-specific properties (no call loss, no cyclic call forwarding, no infeasible paths) as well as user-defined properties for CPL programs.

  • Verification of OS schedulers (Acadie, Obasco, DIKU)

The Bossa language allows a system programmer to easily implement schedulers for processes of operating systems. First, a system expert defines the possible process transitions in the form of automata. Second, the programmer implements a specific scheduling strategy. The verification problem consists in ensuring that these schedulers respect the constraints prescribed by the system expert. While static analysis has traditionally been used for this purpose, it is not sufficiently powerful to guarantee correctness. Standard model checking, however, can only be used for finite-state instances. In joint work with the Acadie team, a counter abstraction has been designed for this problem that can be verified with the Mona tool in WS1S. A bug has been found in the Bossa description of a Linux scheduler.

  • Verification of distributed algorithms (Acadie, Mosel, MSR)

Several case studies have been carried out for the verification of classical distributed algorithms (such as group membership, termination detection, and consensus) in TLA+, using model checking as well as interactive theorem proving. A novel work in this direction is the definition of a high-level algorithmic language for distributed algorithms that is compiled to TLA+ for later verification. This language extends Lamport's +CAL for the case of distributed programming.

  • Work related to VeriTLA+

The Obasco and DIKU teams have been working on the Coccinelle project on semantic patches for driver evolution and have cooperated with D. Doligez on verification issues for such patches.

The Acadie and Mosel teams have worked on type checking and type inference for TLA+, which is originally untyped and set based. The challenge is to come up with a reasonably permissive, but still machine-checkable type system to catch trivial errors before model checking.


[modifier]

Publications

  • J.P. Bodeveix, M. Filali, J.L. Lawall, G. Muller: Automatic Verification of Bossa Scheduler Properties. AVOCS, Electronic Notes in Theoretical Computer Science 185: 17-32 (2007). url
  • M. Filali: A Mechanization of Phylogenetic Trees. 4th Intl. Verification Workshop (Verify '07), Bremen, 2007. url
  • P. Fontaine, J.-Y. Marion, S. Merz, L. Prensa Nieto, A. Tiu: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006), LNCS 3920. pdf
  • F. Latry, J. Mercadal, C. Consel: Processing Domain-Specific Modeling Languages - A Case Study in Telephony Services. Generative Programming and Component Engineering for QoS Provisioning in Distributed Systems (GPCE4QOS), Portland, Oregon, October 2006. pdf
  • S. Merz, M. Notti: Prototypical Proof Manager for TLA+. Internship report, INRIA Nancy Grand Est, July 2007. pdf
  • S. Mouelhi, S. Merz, M. Quinson: Formal verification of distributed algorithms using +CAL. Technical Report, INRIA Nancy Grand Est, August 2007.
  • Y. Padioleau, R. Rydhof Hansen, J. L. Lawall, G. Muller: Semantic Patches for Documenting and Automating Collateral Evolutions in Linux Device Drivers. Linguistic Support for Modern Operating Systems (PLOS 2006), San Jose, California, October 2006. pdf
  • Y. Padioleau, J. L. Lawall, G. Muller: Semantic Patches, Documenting and Automating Collateral Evolutions in Linux Device Drivers. Ottawa Linux Symposium, June 2007.
  • H. Stuart, R. Rydhof Hansen, J. L. Lawall, J. Andersen, Y. Padioleau, G. Muller: Towards Easing the Diagnosis of Bugs in OS Code. 4th Workshop on Programming Languages and Operating Systems (PLOS 2007), Stevenson, Washington, October 2007.
Récupérée de « http://wiki.loria.fr/wiki/VeriTLA »
Outils personels