基于混成自动机的cps构件服务组合建模与验证

《基于混成自动机的cps构件服务组合建模与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、万方数据苏州大学学位论文独创性声明本人郑重声明：所提交的学位论文是本人在导师的指导下，独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本论文不含其他个人或集体己经发表或撰写过的研究成果，也不含为获得苏州大学或其它教育机构的学位证书而使用过的材料。对本文的研究作出重要贡献的个人和集体，均已在文中以明确方式标明。本人承担本声明的法律责任。论文作者签名：圣遮童日期：研丛15-万方数据苏州大学学位论文使用授权声明～一本人完全了解苏州大学关于收集、保存和使用学位论文的规定，即：学位论文著作权归属苏卅l大学。本学位论文电子文档的内容和纸质论文的内容相一致。苏州大学有权

2、向国家图书馆、中国社科院文献信息情报中心、中国科学技术信息研究所(含万方数据电子出版社)、中国学术期刊(光盘版)电子杂志社送交本学位论文的复印件和电子文档，允许论文被查阅和借阅，可以采用影印、缩印或其他复制手段保存和汇编学位论文，可以将学位论文的全部或部分内容编入有关数据库进行检索。涉密论文口本学位论文属在——年一月解密后适用本规定。非涉密论文口论文作者签名：圣缝S日导师签名：期：垒纷!!签日期：?堂∥扩万方数据基于混成自动机的CPS构件服务组合建模与验证中文摘要信息．物理融合系统(Cyber-PhysicalSystem，CPS)是一种包含了嵌入式、控制、通信以及

3、海量数据处理等技术的复杂的网络化嵌入式系统，它和物联网被认为是信息产业未来的发展方向。CPS被广泛应用在安全攸关领域，这些领域对系统可靠性具有极高的要求，因此如何保障CPS的可靠性成为一个研究热点。形式化方法是提高系统可靠性的一种有效方法，主要包括形式化建模与形式化验证两方面。由于CPS是复杂的系统，对其整体建模与验证会非常困难，针对这一问题，本文采用组合建模与验证的思路，首先将CPS分解为原子构件，再将其提供的服务建立为原子构件服务模型，然后验证原子构件服务模型的相关性质，最后建立组合服务模型并对其性质进行验证。根据上述思路，本文主要工作包括以下三个方面：(1)分

4、析CPS的相关性质，基于混成自动机建立CPS原子构件服务模型，并分析其相关性质；(2)在CPS原子构件服务模型的基础之上，建立其组合服务模型；(3)对组合服务模型的同步／异步通信以及死锁检测进行验证，其中通信和死锁是影响系统可靠性的重要因素。最后，通过一个实例说明该模型的有效性。关键词：混成自动机；信息．物理融合系统；构件服务组合；形式化建模；形式化验证作者：张建宁指导老师：张广泉万方数据英文摘要基于混成自动机的CPS构件服务组合建模与验证ModelingandVerifyingofCPSComponentServiceCompositionBasedonHybri

5、dAutomataAbstractTheCyber-PhysicalSystem(CPS)isakindofnetworkedembeddedsystemwhichconsistsofembeddedtechnology,controltechnology,communicationtechnologyandbigdataanalysistechnology．It’SconsideredthattheCPSandInteractofThings(IoT)willbefuturedirectionsoftheinformationindustry．CPSiswidel

6、yusedinsafetycriticalfields，andthesefieldshavehighrequirementsofsystemreliability．Therefore，it’SahotspotinCPSresearchthathowtoensurethereliabilityofCPS．Formalmethodisallimportantmethodtoimprovesystemreliability，anditmainlycontainsformalmodelingandverifying．SinceCPSisSOcomplexthatit’Sha

7、rdlytobemodeledandanalyzed，SOweusethecompositionalverificationmethodtocopeWiththisproblem．First,wedividetheCPSintoatomcomponents，andthenmodeltheservicesofatomcomponentsascomponent-service．Second，weverifythepropertiesofthecomponent-servicemodels．Atlast，wemodelthecompositionalserviceba