Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
McErlang: a model checker for a distributed functional programming language
Año:2007
Áreas de investigación
  • Lenguaje de programación
Datos
Descripción
We present a model checker for verifying distributed programs written in the Erlang programming language. Providing a model checker for Erlang is especially rewarding since the language is by now being seen as a very capable platform for developing industrial strength distributed applications with excellent failure tolerance characteristics. In contrast to most other Erlang verification attempts, we provide support for a very substantial part of the language. The model checker has full Erlang data type support, support for general process communication, node semantics (inter-process behave subtly different from intra-process communication), fault detection and fault tolerance through process linking, and can verify programs written using the OTP Erlang component library (used by most modern Erlang programs). As the model checking tool is itself implemented in Erlang we benefit from the advantages that a (dynamically typed) functional programming language offers: easy prototyping and experimentation with new verification algorithms, rich executable models that use complex data structures directly programmed in Erlang, the ability to treat executable models interchangeably as programs (to be executed directly by the Erlang interpreter) and data, and not least the possibility to cleanly structure and to cleanly combine various verification sub-tasks. In the paper we discuss the design of the tool and provide early indications on its performance.
Internacional
Si
Nombre congreso
12th ACM SIGPLAN International conference on functional programming (ICFP 2007)
Tipo de participación
960
Lugar del congreso
Freiburg, Germany
Revisores
Si
ISBN o ISSN
978-1-59593-815-2
DOI
Fecha inicio congreso
Fecha fin congreso
Desde la página
Hasta la página
Título de las actas
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Hans Svensson (Computer Science and Engineering, Chalmers University of Technology, Sweden (Gothenburg))
  • Autor: Lars-Ake Fredlund (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)