The Credo methodology (extended version)

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

Contributors

  • Immo Grabe - , National research institute for mathematics and computer science in the Netherlands (Author)
  • Mohammad Mahdi Jaghoori - , National research institute for mathematics and computer science in the Netherlands (Author)
  • Joachim Klein - , Chair of Algebraic and Logical Foundations of Computer Science (Author)
  • Sascha Klüppelholz - , Chair of Algebraic and Logical Foundations of Computer Science (Author)
  • Andries Stam - (Author)
  • Christel Baier - , Chair of Algebraic and Logical Foundations of Computer Science (Author)
  • Tobias Blechmann - , TUD Dresden University of Technology (Author)
  • Bernhard K. Aichernig - , United Nations (Author)
  • Frank De Boer - , National research institute for mathematics and computer science in the Netherlands (Author)
  • Andreas Griesmayer - , United Nations (Author)
  • Einar Broch Johnsen - , University of Oslo (Author)
  • Marcel Kyas - , Free University of Berlin (Author)
  • Wolfgang Leister - , Norwegian Computing Centre (Author)
  • Rudolf Schlatte - , University of Oslo (Author)
  • Martin Steffen - , University of Oslo (Author)
  • Simon Tschirner - , Uppsala University (Author)
  • Liang Xuedong - , Oslo University Hospital Rikshospitalet (Author)
  • Wang Yi - , Uppsala University (Author)

Abstract

This paper is an extended version of the Credo Methodology [16]. Credo offers tools and techniques to model and analyze highly reconfigurable distributed systems. In a previous version we presented an integrated methodology to use the Credo tool suite. Following a compositional, component-based approach to model and analyze distributed systems, we presented a separation of the system into components and the network. A high-level, abstract representation of the dataflow level on the network was given in terms of behavioral interface automata and a detailed model of the components in terms of Creol models. Here we extend the methodology with a detailed model of the network connecting these components. The Vereofy tool set is used to model and analyze the dataflow of the network in detail. The behavioral automata connect the detailed model of the network and the detailed model of the components. We apply the extended methodology to our running example, a peer-to-peer file-sharing system.

Details

Original languageEnglish
Title of host publicationFormal Methods for Components and Objects
EditorsFrank S. Boer, Marcello M. Bonsangue, Stefan Hallerstede, Michael Leuschel
PublisherSpringer-Verlag
Pages41-69
Number of pages29
ISBN (electronic)978-3-642-17071-3
ISBN (print)3642170706, 978-3-642-17070-6
Publication statusPublished - 2010
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume6286 LNCS
ISSN0302-9743

External IDs

dblp conf/fmco/GrabeJKKSBBABG09
Scopus 78650194035
ORCID /0000-0002-5321-9343/work/180369921
ORCID /0000-0003-1724-2586/work/180372475

Keywords

Keywords

  • distributed systems, testing, schedulability analysis, dynamic reconfiguration, compositional verification

Library keywords