VeriTLA Intern

Un article de Loria Wiki.

[modifier]

Automatic techniques for the verification of SPL programs

The SIP protocol is an application-level protocol designed to initiate, terminate, and modify interactive sessions for telephony that may also include multimedia elements. It is currently the leading signalling protocol standard for Voice over IP telephony, playing a role analogous to that of the HTTP protocol for the Web, and it is widely supported, for example by a Java API. Because SIP is a rather complex protocol and application development requires expertise in networking, distributed systems, and the underlying platform, programming SIP applications is complex and prone to errors that may lead to unacceptable failures (lost calls, inconsistency with the underlying protocol state machine etc).

SPL (session programming language, papers available) is a domain-specific language for application development based on SIP. It provides specific abstractions that harness the power of SIP and is designed to simplify the validation of basic correctness properties of applications. In previous work (see publication by Latry et al.), a subset of SPL has been formalized in the modeling language TLA+, and the TLA+ model checker has been used to verify some key correctness properties. It became clear that many properties can be usefully verified using automatic theorem provers, including SMT (satisfiability modulo theory) solvers. Typical correctness properties for SPL programs include no loss of calls, acyclic forwarding chains, or the presence of a signaling action in any execution path.

The objectives of this internship are to experiment this approach in some more detail:

  • identify suitable abstractions for the formal verification of correctness properties by automatic theorem proving, in particular SMT (satisfiability modulo theories) solvers,
  • generate proof obligations from SPL programs for the verification of standard properties, and have them verified by the prover,
  • evaluate the possibility of presenting simple justifications to the user in case the proof fails, based on the counter-model generated by the tool.

This internship is part of the VeriTLA+ project on developing domain-specific verification support for domain-specific languages, including SPL. The design of a verification platform for TLA+ is the goal of a joint project between INRIA and Microsoft Research.

Background: The candidate should have an inclination for formal reasoning and for modeling systems. Previous experience with theorem provers is a plus, but is not required.

Duration: 3 months

Location: LORIA, Nancy, France

Supervision: Stephan Merz, assisted by Charles Consel for SPL

References:

  • SIP protocol
  • C. Consel and L. Réveillère: A DSL Paradigm for Domains of Services -- A Study of Communication Services. In: Domain-Specific Program Generation. Lecture Notes in Computer Science 3016, pages 165-179. Springer, 2004.
  • 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.
  • L. Lamport: Specifying Systems. Addison-Wesley, 2002. See also the TLA+ home page.
  • S. Merz: On the Logic of TLA+. Computers and Informatics 22, pp. 351-379 (2003).
Récupérée de « http://wiki.loria.fr/wiki/VeriTLA_Intern »
Outils personels