A model checking-based approach for security policy verification of mobile systems

DOI10.1007/s00165-010-0159-yzbMath1242.68153OpenAlexW2045440241MaRDI QIDQ432137

Chiara Braghin, Natasha Sharygina, Katerina Barone-Adesi

Publication date: 3 July 2012

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

Full work available at URL: https://doi.org/10.1007/s00165-010-0159-y

zbMATH Keywords

mobile systemssoftware verificationaccess controlinformation flowprogram security and safetysecurity policies

Mathematics Subject Classification ID

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

Related Items

A UTP approach for rTiMo, A model checking-based approach for security policy verification of mobile systems, UTP Semantics for rTiMo

Uses Software

• BLAST
• SLAM
• SPIN
• ComFoRT
• Java PathFinder
• Bebop
• KLAIM
• TLPVS
• SatAbs
• MAGIC
• Aglets

Cites Work

• TLPVS
• A model checking-based approach for security policy verification of mobile systems
• Mobile ambients
• Model checking JAVA programs using JAVA PathFinder
• Verification of Boolean programs with unbounded thread creation
• Verifying safety properties of concurrent Java programs using 3-valued logic
• CONCUR 2004 - Concurrency Theory
• Model Checking Software
• Static Analysis
• Programming Languages and Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Integrated Formal Methods
• Formal Methods for Open Object-Based Distributed Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item