Model checking the observational determinism security property using PROMELA and SPIN

DOI10.1007/S00165-014-0331-XzbMath1347.68222OpenAlexW1966189394MaRDI QIDQ903490

Mohammad Abdollahi Azgomi, Maryam Dabaghchian

Publication date: 6 January 2016

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

Full work available at URL: https://doi.org/10.1007/s00165-014-0331-x

zbMATH Keywords

model checkinglinear temporal logicSPINinformation flow securityPROMELAobservational determinism

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

• SPIN

Cites Work

• Unnamed Item
• Model Checking Information Flow in Reactive Systems
• A lattice model of secure information flow
• Logic in Computer Science
• Model Checking on Trees with Path Equivalences
• Static Analysis

This page was built for publication: Model checking the observational determinism security property using PROMELA and SPIN