DSpace UNL

Faculdade de Ciências e Tecnologia (FCT) >
FCT Departamentos >
FCT: Departamento de Informática >
FCT: DI - Dissertações de Mestrado >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10362/4023

Título: A behavioral analysis tool for models of software systems
Autor: Silva, Ricardo João Besteiro e
Orientador: Caires, Luís
Palavras-chave: Bisimulation algorithm
Model checking
Process calculi
Characteristic formula
Issue Date: 2010
Editora: Faculdade de Ciências e Tecnologia
Resumo: Process calculi are simple languages which permit modeling of concurrent systems so that they can be verified for correctness. We can analyze concurrent systems based on process calculi by either comparing a representation of the actual implementation with a simpler specification for equivalence, or by verifying whether desired properties described in an adequate logic hold. Strong bisimulation equivalence is one of many equivalence relations defined on process calculi to aid in the verification of concurrent software. This equivalence relation relates processes which exhibit the same behavior, i.e. perform the same transitions, as equivalent regardless of internal implementation details. Logics to reason about processes range from those which describe temporal properties – how properties evolve during the course of a process’ life – behavioral properties – which actions a process is capable of performing – and spatial properties – what components compose a process and how are they connected. Model checking consists of verifying if a model, in our case a process, satisfies a given property. Model checking techniques are quite popular in conjunction with process calculi to aid in the verification of the correctness of concurrent systems. In this thesis we address the problems of checking bisimilarity between processess using characteristic formulae, which are formulae used to fully describe a process’ behavior. We implement some facilities to allow bisimilarity verification in the Spatial Logic Model Checker tool. As a result of adding these facilities we also extend the SLMC tool with an extra modality in the logic it uses to reason about processes. We have also added the possibility to define mutually recursive properties in the tool and enhanced the model checking algorithm with a cache to prevent redundant, time-consuming checks to be performed.
Descrição: Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática
URI: http://hdl.handle.net/10362/4023
Appears in Collections:FCT: DI - Dissertações de Mestrado

Files in This Item:

File Description SizeFormat
Silva_2010.pdf274,85 kBAdobe PDFView/Open

Please give feedback about this item
FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Logotipo do DeGóis 

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.


Universidade Nova de Lisboa  - Feedback
Promotores do RCAAP   Financiadores do RCAAP

Fundação para a Ciência e a Tecnologia Universidade do Minho   Governo Português Ministério da Educação e Ciência PO Sociedade do Conhecimento (POSC) Portal oficial da União Europeia