Please use this identifier to cite or link to this item:
Title: A behavioral analysis tool for models of software systems
Author: Silva, Ricardo João Besteiro e
Advisor: Caires, Luís
Keywords: Bisimulation algorithm
Model checking
Process calculi
Characteristic formula
Defense Date: 2010
Publisher: Faculdade de Ciências e Tecnologia
Abstract: 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.
Description: Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática
Appears in Collections:FCT: DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Silva_2010.pdf274,85 kBAdobe PDFView/Open

FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

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