A framework for specifying and verifying the behaviour of open systems

DOI10.1016/j.jlap.2004.05.004zbMath1080.68074OpenAlexW1996632489WikidataQ62046308 ScholiaQ62046308MaRDI QIDQ1779319

Franco Turini, Andrea Bracciali, Antonio Brogi

Publication date: 1 June 2005

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlap.2004.05.004

zbMATH Keywords

VerificationOpen systemsProcess algebras

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Uses Software

• Rapide
• MANIFOLD
• KLAIM

Cites Work

• A calculus of mobile processes. I
• A calculus for cryptographic protocols: The spi calculus
• Testing equivalences for processes
• Comparing syntactic and semantic action refinement
• Bisimulation by Unification*
• Communicating sequential processes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item