毕业设计（论文）进程交互消息可见性研究.docVIP

PAGE \* ROMAN IV 摘 要 交错并发是复杂的进程演算，包括顺序组合、选择组合和并行组合演算。交互进程特性之一是进程之间交互消息的可见性。 阐述进程演算语言，将其代数表达式表达为标记变迁系统，并得到相应的变迁图；论述进程演算语言的结构化操作语义。 在进程代数表达式及其结构化操作语义下，讨论进程互模拟和互模拟等价问题；在动作细化下，讨论进程互模拟等价的保持问题，并对系统进行约简。 将进程之间交互消息的可见与否标记为并发交错进程系统的外部动作和内部动作。在进程代数表达式及其结构化操作语义下，区分外部动作和内部动作。 给出了消息可见与不可见的例，分别讨论了通信系统和必威体育官网网址通信系统的消息可见性问题，并针对群内成员之间和多个群成员之间的消息交互进行了分析。 关键词：交互进程；消息可见性；形式化方法 Abstract Interleaved concurrency is a complex process calculus that includes sequential combinations, choice combinations, and parallel combinatorial calculus. One of the features of the interaction process is visibility of interactive messages between processes. The process calculus language is described, whose algebraic expressions are expressed as labeled transition systems, and corresponding transition graphs are given. In the process algebra expression and its structured operation semantics, the problem of mutual simulation and bisimulation equivalence is discussed. Under the action refinement, the problem of the equivalence of process bisimulation equivalence is discussed and the system is reduced. The interaction messages are marked between processes as external actions and internal actions of concurrent interleaved process systems. In the process algebraic expression and its structured operation semantics, are distinguished between external and internal actions. The visible and invisible cases are given, the problem of message visibility communication system and secure communication system are discussed, and the between group members and group members of the message exchange is analyzed. Key words: interactive processes; message visibility; formal methods 目 录 TOC \o HYPERLINK \l _Toc483653548 摘 要 PAGEREF _Toc483653548 \h \* Arabic 1 HYPERLINK \l _Toc483653549 Abstract PAGEREF _Toc483653549 \h \* Arabic 2 HYPERLINK \l _Toc483653551 目录 PAGEREF _Toc483653551 \h \* Arabic 3 HYPERLINK \l _Toc483653552 图目录 PAGEREF _Toc483653552 \h \* Arabic 3 HYPERLINK \l _Toc483653553 第一章 绪 论 PAGEREF _Toc48