Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
Model-Checking Erlang - A Comparison between EtomCRL2 and McErlang
Año:2010
Áreas de investigación
  • Ciencias de la computación y tecnología informática
Datos
Descripción
Model-checking programs is important in the development of a reliable software system. Two approaches might be applied to model-check a system at a source code level. One is to directly apply model-checking algorithm to the programming language; the other to abstract the program source codes into a formal specification, upon which some standard model-checkers can be used to verify system's properties. Both methods have recently been investigated for model-checking the functional programming language Erlang. Correspondingly, two Erlang model-checkers McErlang and Etomcrl2 are developed. This paper evaluates the two model-checkers by applying them to verify a a distributed and concurrent example - telecoms implemented in Erlang/OTP. A number of system key properties are model-checked with both tool-sets. Advantages and disadvantages upon the uses of Etomcrl2 and McErlang are compared and summarized. Through such a case study, we intend to evaluate the two model-checkers on their effectiveness when verifying distributed and concurrent systems, and propose suggestions for their future work.
Internacional
No
Nombre congreso
TAIC PART 2010
Tipo de participación
960
Lugar del congreso
Windsor, UK
Revisores
Si
ISBN o ISSN
3-642-15584-7
DOI
Fecha inicio congreso
03/09/2010
Fecha fin congreso
05/09/2010
Desde la página
23
Hasta la página
38
Título de las actas
Testing - practice and research techniques (TAIC PART 2010)
Esta actividad pertenece a memorias de investigación
Participantes
  • Autor: Lars-Ake Fredlund (UPM)
  • Autor: Qiang Guo (Department of Computer Science, The University of Sheffield, UK)
  • Autor: Clara Benac Earle (UPM)
  • Autor: John Derrick (Department of Computer Science, The University of Sheffield, UK)
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
S2i 2021 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)