Model checking of ambient calculus specifications against ambient logic formulas

Abstract

Formal methods are mathematical techniques applied in specification and verification of concurrent interactive systems. Model checking is a widely used formal method for formal verification of systems. In model checking, an exhaustive search is applied on a nite state model of the target system. While there are model checkers to verify the only temporal behaviors of systems, two new notions of model checking analysis recently come into prominence, mobility and locations. Although there are various model checker proposals for modeling and verifying concurrent interactive systems with respect to mobility and locations, there are a few model checker tools able to perform such verifications. In this thesis, a new model checking methodology is proposed which is able to verify temporal and spatial properties of systems together. The proposed model checking methodology is able to perform more detailed verifications than existing tools. In this thesis, ambient logic and ambient calculus are used as formal languages to express models and the properties of the systems. Ambient calculus is a process calculus derived from calculus. It is able to theorize about concurrent systems with respect to mobility and locations. Ambient logic is a modal logic able to express temporal and spatial properties of models. It is strictly based on ambient calculus. Proposed model checking methodology accepts models expressed with a fragment of ambient calculus and properties expressed with a fragment of ambient logic as inputs. It returns a success message or the states of the model which are violating properties. In the scope of this thesis, an implementation of proposed methodology is provided v which is the only tool using both ambient calculus and ambient logic. In this thesis, performance of the proposed model checking methodology is shown over case studies. Security policies de ned for multi-domain networks need to be formally checked against security breaches and ensured that they are consistent in a given network con guration. In case studies, a set of ambient calculus speci cations modeling such networks are veri ed against ambient logic formulas with proposed model checking methodology.