Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Parameterized Systems in BIP: Design and Model Checking
 
conference paper

Parameterized Systems in BIP: Design and Model Checking

Konnov, Igor
•
Kotek, Tomer
•
Wang, Qiang  
Show more
Desharnais, Josée
•
Jagadeesan, Radha
2016
Proceedings of the 27th International Conference on Concurrency Theory (CONCUR 2016)
27th International Conference on Concurrency Theory (CONCUR 2016)

BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to systems parameterized in the number of components. We show that FOIL captures classical parameterized architectures such as token-passing rings, cliques of identical components communicating with rendezvous or broadcast, and client-server systems. Although the BIP framework includes efficient verification tools for statically-defined systems, none are available for parameterized systems with an unbounded number of components. The parameterized model checking literature contains a wealth of techniques for systems of classical architectures. However, application of these results requires a deep understanding of parameterized model checking techniques and their underlying mathematical models. To overcome these difficulties, we introduce a framework that automatically identifies parameterized model checking techniques applicable to a BIP design. To our knowledge, it is the first framework that allows one to apply prominent parameterized model checking results in a systematic way.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

main.pdf

Access type

openaccess

Size

280.13 KB

Format

Adobe PDF

Checksum (MD5)

72e39eaf44d13289a4b464be4cc29668

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés