共查询到16条相似文献,搜索用时 93 毫秒
1.
2.
形式描述技术在协议设计中的应用是至关重要的和必不可少的,为形式规范确定一个合适的结构又是应用此技术的关键步骤,基于此文中重点研究了基于LOTOS技术的形式结构模型的创建方法.简要介绍了开发网络协议的形式描述技术、网络协议的结构概念、等级抽象和LOTOS描述规范风格.基于LOTOS技术,提出了网络协议开发过程中形式结构模型的创建原则和方法,此方法结合LOTOS语言特征,应用其描述规范风格,融协议结构、逐步改进和等级抽象为一体,简化了所开发协议的验证、测试和实现的复杂性. 相似文献
3.
LOTOS形式规范的目标实现是协议设计中必不可少的阶段之一。该文对基于LOTOS的形式描述规范的实现方法进行了研究,包括目标实现环境的特点、实现中的空白因素、抽象模型到实现模型的转换、规范的最终目标实现,并对如何将LOTOS规范转换为C、C 语言实现进行了探讨。 相似文献
4.
形式描述技术在协议设计中的应用是至关重要的和必不可少的,为形式规范确定一个合适的结构又是应用此技术的关键步骤,基于此文中重点研究了基于LOTOS技术的形式结构模型的创建方法。简要介绍了开发网络协议的形式描述技术、网络协议的结构概念、等级抽象和LOTOS描述规范风格。基于LOTOS技术,提出了网络协议开发过程中形式结构模型的创建原则和方法,此方法结合LOTOS语言特征,应用其描述规范风格,融协议结构、逐步改进和等级抽象为一体,简化了所开发协议的验证、测试和实现的复杂性。 相似文献
5.
肖军模 《计算机工程与应用》1987,(1)
本文介绍ISO最新开发的一种形式描述技术——LOTOS语言,这种语言以数学方法描述进程外观行为的时态次序,它定义了以事件为运算对象对行为表达式进行运算的一整套规则和相应的形式证明规则,从而为协议的正确说明与验证打下了基础。本文介紹事件和进程的描述方法,以及行为表达式的证明方法。读者可以发现,LOTOS有更广泛的应用。 相似文献
6.
通信协议形式化模型的研究 总被引:5,自引:0,他引:5
本文提出了适应于通信协议的一类抽象形式化模型:抽象行为模型和抽象结构模型.前者主要包括事件、输入/输出、内部/外部和状态等子模型;后者主要包括交互点和分层子模型.文中讨论了这类形式模型的有效性和适用性,运用该类模型对通信协议的主要概念及性质进行了形式定义和描述.重点给出了基于该类模型的协议安全性及活性的形式定义,研讨了安全性及活性的验证,以及某些典型形式描述技术FDT(Estelle,LOTOS,SDL)之间的语义联系,从而为通信协议的研究提供了一种有效的形式基础. 相似文献
7.
ISO/OSI会话层标准的形式化描述和开发 总被引:1,自引:0,他引:1
沈立涛 《计算机工程与设计》1989,(5):30-39
本文通过对形式化描述技术LOTOS语言和ISO/OSI会话层标准的简要介绍,较详细地讨论了用LOTOS语言对OSI会话层的形式化规范描述,给出了其结构模型及一些重要的模块结构描述。 相似文献
8.
为了实现由BPEL描述的Web服务组合到LOTOS的自动化转换, 提出一种基于翻译模式的转换算法。从BPEL语言的XML schema定义出发, 分析BPEL本身的语言结构, 得到BPEL语言的产生式。再根据BPEL到LOTOS的语义映射规则, 设计BPEL到LOTOS的翻译模式。同时, 在基本映射规则之上, 给出BPEL到LOTOS的数据类型和故障处理机制的转换规则。最后结合Web服务实例, 验证该工具的可行性。 相似文献
9.
10.
11.
Vijay Varadharajan 《Computer Standards & Interfaces》1990,9(3):203-215
Formal specification techniques have been employed over the past decade or so by various workers in data communication and computer network systems in order to provide both definitional specifications of protocols and models of protocols for analytic purposes. This paper considers the use of the specification language LOTOS (Language of Temporal Ordering Specification) for specifying some authentication protocols developed in the security field. The language LOTOS recently became an International ISO Standard and the protocols specified form part of the ISO and CCITT Standards. In fact, the CCITT protocol which is considered in this paper, has been used in the LOCATOR (X.400 Secure Mail) project within HPLabs. We first give a brief introduction to LOTOS and then specify two security protocols from ISO/DP 9798 and CCITT X.509 Standards. We feel that a formal specification of protocols is a useful and a necessary step towards understandability, analysis and implementation of the protocols. Further, we feel that LOTOS possesses the necessary features required for specifying such protocols. 相似文献
12.
UML diagrams are the conventional methods for visual modeling systems. Among them, the Statechart diagrams are used to show the runtime behavior of a system, but the correctness of such diagrams is the primary concern of the designers because of concurrency issues like livelock, inaccessible states, and non-deterministic states. Process algebra methods have the capabilities that are suitable for verification and validation of Statecharts. To this end, in this paper, process algebra language LOTOS (Language Of Temporal Ordering Specification) is used as the target language, and a method is presented to map UML Statecharts to the LOTOS processes, called USLP. Then the correctness of the proposed mappings is proved by demonstrating the isomorphism relation between the Labeled Transition System (LTS) of a Statechart and the LTS of its transformed LOTOS specification. Next, tools CADP (Construction and Analysis of Distributed Processes) is used for verification and validation of the mapped LOTOS models, and the CSP process algebra and its tools, FDR are used to verify the properties could not be verified by the LOTOS and its toolset. The experimental results show our approach can: (1) verify some properties (the issues) that are not verified by other approaches and (2) reduce the space that should be searched to verify the properties. 相似文献
13.
Monika Kapus-Kolar 《Distributed Computing》1999,12(4):175-177
Summary. An algorithm by Kant, Higashino and Bochmann for service-based protocol synthesis in the standard specification language
LOTOS is discussed. It is demonstrated that the transformations for distributed implementation of synchronised parallel execution
and of disabling are not correct in a general case.
Received: January 1998 / Accepted: January 1999 相似文献
14.
LOTOS is an executable specification language for distributed systems currently being standardized within ISO as a tool for the formal specification of open systems interconnection protocols and services. It is based on an extended version of Milner's calculus of communicating systems (CCS) and on ACT ONE abstract data type (ADT) formalism. A brief introduction to LOTOS is given, along with a discussion of LOTOS operational semantics, and of the executability of LOTOS specifications. Further, an account of a prototype LOTOS interpreter is given, which includes an interactive system that allows the user to direct the execution of a specification (for example, for testing purposes). The interpreter was implemented in YACC/LEX, C and Prolog. The following topics are discussed: syntax and static semantics analysis; translation from LOTOS external format to internal representation; evaluation of ADT value expressions and extended CCS behaviour expressions. It is shown that the interpreter can be used in a variety of ways: to recognize whether a given sequence of interactions is allowed by the specification; to generate randomly chosen sequences of interactions; in a user-guided generation mode, etc. 相似文献
15.
分布式多媒体系统中的同步问题研究 总被引:8,自引:0,他引:8
金涛 《计算机研究与发展》1999,36(12):1510-1516
文中首先给出基于进程代数的LOTOS形式化规范语言的基本概念,通过对传统LOTOS进行基于时间的扩充,引入时间算子,并给出其相应的语法定义和形式语义。通过对分布式环境下的多媒体同步问题进行系统的分析,利用基于时间扩充的LOTOS,给出了基本的同步问题和严格的多媒体唇同步问题的算法描述。同时给出一个实例系统,进一步描述了基于时间扩充的LOTOS,对分布环境下多媒体信息同步问题在实际中的应用,并与传统 相似文献