Verification of \(\mathrm{EB}^3\) specifications using CADP

DOI10.1007/s00165-016-0362-6zbMath1335.68150OpenAlexW2319022878MaRDI QIDQ282110

Catalin Dima, Radu Mateescu, Frédéric Lang, Dimitris Vekris

Publication date: 12 May 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-016-0362-6

zbMATH Keywords

verificationmodel checkinginformation systemsprocess algebras\(\mathrm{EB}^3\)Lotos NT

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Verification of \(\mathrm{EB}^3\) specifications using CADP, Parameterized verification of monotone information systems

Uses Software

• LOTOS
• SPIN
• NuSMV
• CADP
• Rodin
• ProB
• Atelier B
• FDR2

Cites Work

• Verification of \(\mathrm{EB}^3\) specifications using CADP
• Results on the propositional \(\mu\)-calculus
• Algebra of communicating processes with abstraction
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• Proof-based verification approaches for dynamic properties: application to the information system domain
• CSP theorems for communicating B machines
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• Propositional dynamic logic of looping and converse is elementarily decidable
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Communicating sequential processes
• The B-Book
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item