Observatorio de I+D+i UPM

Memorias de investigación
Communications at congresses:
Model-Checking Erlang - A Comparison between EtomCRL2 and McErlang
Year:2010
Research Areas
  • Information technology and adata processing
Information
Abstract
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.
International
No
Congress
TAIC PART 2010
960
Place
Windsor, UK
Reviewers
Si
ISBN/ISSN
3-642-15584-7
Start Date
03/09/2010
End Date
05/09/2010
From page
23
To page
38
Testing - practice and research techniques (TAIC PART 2010)
Participants
  • 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)
Research Group, Departaments and Institutes related
  • Creador: Grupo de Investigación: BABEL: Desarrollo de Software Fiable y de Alta Calidad a partir de Tecnología Declarativa
S2i 2019 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)