Arşiv ve Dokümantasyon Merkezi
Dijital Arşivi

Model checking of ambient calculus specifications against ambient logic formulas

Basit öğe kaydını göster

dc.contributor Graduate Program in Computer Engineering.
dc.contributor.advisor Çağlayan, M. Ufuk.
dc.contributor.author Akar, Ozan.
dc.date.accessioned 2023-03-16T10:00:07Z
dc.date.available 2023-03-16T10:00:07Z
dc.date.issued 2009.
dc.identifier.other CMPE 2009 A32
dc.identifier.uri http://digitalarchive.boun.edu.tr/handle/123456789/12144
dc.description.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.
dc.format.extent 30cm.
dc.publisher Thesis (M.S.)-Bogazici University. Institute for Graduate Studies in Science and Engineering, 2009.
dc.relation Includes appendices.
dc.relation Includes appendices.
dc.subject.lcsh Computer software -- Development.
dc.subject.lcsh Formal methods (Computer science)
dc.title Model checking of ambient calculus specifications against ambient logic formulas
dc.format.pages xv, 70 leaves;


Bu öğenin dosyaları

Bu öğe aşağıdaki koleksiyon(lar)da görünmektedir.

Basit öğe kaydını göster

Dijital Arşivde Ara


Göz at

Hesabım