Model-Checking Helena Ensembles with Spin

DOI10.1007/978-3-319-23165-5_16MaRDI QIDQ2945715zbMATH OpenOpenAlexFDO

Authors Rolf Hennicker, Annabelle Klarl, Martin Wirsing

Publication date 14 September 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-23165-5_16

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)

Recommendations

• scientific article; zbMATH DE number 1744968
• Model checking Paxos in Spin
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• Model checking the observational determinism security property using PROMELA and SPIN

Cites work

• scientific article; zbMATH DE number 3776831 (Why is no real title available?)
• scientific article; zbMATH DE number 1283472 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A formal approach to object-oriented software engineering
• Algebraic simulations
• Foundations for ensemble modeling -- the Helena approach. Handling massively distributed systems with elaborate ensemble architectures
• Programming and verifying component ensembles
• The fork calculus
• What Is a Multi-modeling Language?

Cited in

(3)

• Programming and verifying component ensembles
• Role-based development of dynamically evolving esembles
• Foundations for ensemble modeling -- the Helena approach. Handling massively distributed systems with elaborate ensemble architectures

Describes a project that uses

Uses Software

• Helena
• SCELlight
• SPIN

This page was built for publication: Model-Checking Helena Ensembles with Spin

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945715)