Model checking of component connectors

Leiden Repository

Model checking of component connectors

Title: Model checking of component connectors
Author: Izadi, Mohammad
Issue Date: 2011-11-06
Keywords: Automata theory
Component connectors
Compositional minimization
Coordination models
Formal verification
Model checking
Symbolic model checking
Abstract: We present a framework for automata theoretic model checking of coordination systems specified in Reo coordination language. To this goal, we introduce Buchi automata of records (BAR) and their augmented version (ABAR) as an operational modeling formalism that covers several intended forms of behavior of Reo connectors, such as fairness, I/O synchronization, and context dependency. To specify the properties to be verified, we introduce an action based linear temporal logic, interpreted over the executions of augmented Buchi automata of records, and show how the formulas can be translated into ABARs. This translation can be done either inductively, or by using an on-the-fly method. To deal with the large state spaces, we show that ABARs can be implemented using ordered binary decision diagrams (OBDD). For this purpose, we also introduce the necessary modifications over the basic model checking algorithm that can be applied directly over OBDD structures. Our implementation and a number of case studies that we carried out show the applicability of our method over large state spaces. We also show that the state explosion problem can be tackled by compositional minimization methods using some suitable equivalence relations. In fact, we show two equivalences that are congruencies with respect to the connector composition operators and such that they both preserves linear time temporal logic properties.
Description: Promotors: Farhad Arbab, Ali Movaghar, Co-promotor: Marcello M. Bonsangue
With summary in Dutch
Faculty: Faculteit der Wiskunde en Natuurwetenschappen
Citation: Izadi, M., 2011, Doctoral thesis, Leiden University
Series/Report no.: IPA Dissertation Series;2011-22
Sponsor: IPA (Institute for Programming research and Algorithmics)
Handle: http://hdl.handle.net/1887/18189
 

Files in this item

Description Size View
application/pdf Thesis 2.662Mb View/Open
application/pdf Cover 97.04Kb View/Open
application/pdf Title page_Contents_List of figures 87.85Kb View/Open
application/pdf Chapter 1 Introduction 88.69Kb View/Open
application/pdf Chapter 2 106.5Kb View/Open
application/pdf Chapter 3 249.6Kb View/Open
application/pdf Chapter 4 352.7Kb View/Open
application/pdf Chapter 5 464.0Kb View/Open
application/pdf Chapter 6 172.8Kb View/Open
application/pdf Chapter 7 1.468Mb View/Open
application/pdf Chapter 8 224.4Kb View/Open
application/pdf Chapter 9 Conculsion and future work 63.33Kb View/Open
application/pdf Bibliography 85.19Kb View/Open
application/pdf Abstract 25.55Kb View/Open
application/pdf Summary in Dutch 25.65Kb View/Open
application/pdf Curriculum Vitae 21.10Kb View/Open
application/pdf Titles in the IPA Dissertation Series 61.57Kb View/Open
application/pdf Propositions 20.80Kb View/Open

This item appears in the following Collection(s)