Checking the Conformance of a Promela Design to its Formal Specification in Event-B

DOI10.1007/978-3-319-17581-2_8zbMath1328.68131OpenAlexW1152386366MaRDI QIDQ3460222

Dieu-Huong Vu, Toshiaki Aoki, Yuki Chiba, Kenro Yatake

Publication date: 6 January 2016

Published in: Communications in Computer and Information Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-17581-2_8

zbMATH Keywords

designformal verificationformal specificationmodel checkingsimulation relation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• GeneSyst
• SPIN
• Rodin
• ProB
• PROMELA
• seL4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Forward and backward simulations. I. Untimed Systems
• Guarded Operations, Refinement and Simulation
• ZB 2005: Formal Specification and Development in Z and B

This page was built for publication: Checking the Conformance of a Promela Design to its Formal Specification in Event-B