摘要：众多的电梯群控系统设计解决方案仅仅基于某一具体功能模块,少有整体系统设计.为此,本文使用Petri网建模工具给出了电梯群控系统的有效模型.该模型除了整体设计外,包括程序设计流程概要建模和局部功能细化,以及电梯低高速的切换和根据交通模式切换不同停留模式的实现细节.最后用s-不变技术、可达标识图等对模型进行了验证.

摘要：在虚拟化技术中,黑客可利用虚拟化监视器(Virtual Machine Monitor)中存在的隐藏信息流窃取用户信息,并且恶意调用(Input/Output,I/O)资源攻击虚拟化监视器.本文以Petri网为系统逻辑设计工具,建立了一种基于Petri网的虚拟化I/O控制模型.该模型解决多个虚拟机争夺共享I/O资源以及虚拟机监视器在管理虚拟机I/O资源的权限时出现的同步问题.本文进一步通过分析Petri网的可达标识图和s_不变量对模型I/O资源间的同步和互斥进行了验证.