首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到16条相似文献,搜索用时 93 毫秒
1.
ELOTOS是协议描述规范语言LOTOS的扩展.本文用标号转换系统LTS(labeledtransitionsystem)给出了ELOTOS的语义.然后,通过对LTS进行踪迹等价住分析,将ELOTOS映射到基于有穷状态机FSM(finitestatemachine)的性能估价模型.  相似文献   

2.
形式描述技术在协议设计中的应用是至关重要的和必不可少的,为形式规范确定一个合适的结构又是应用此技术的关键步骤,基于此文中重点研究了基于LOTOS技术的形式结构模型的创建方法.简要介绍了开发网络协议的形式描述技术、网络协议的结构概念、等级抽象和LOTOS描述规范风格.基于LOTOS技术,提出了网络协议开发过程中形式结构模型的创建原则和方法,此方法结合LOTOS语言特征,应用其描述规范风格,融协议结构、逐步改进和等级抽象为一体,简化了所开发协议的验证、测试和实现的复杂性.  相似文献   

3.
王继曾  张键 《计算机工程》2005,31(12):97-99
LOTOS形式规范的目标实现是协议设计中必不可少的阶段之一。该文对基于LOTOS的形式描述规范的实现方法进行了研究,包括目标实现环境的特点、实现中的空白因素、抽象模型到实现模型的转换、规范的最终目标实现,并对如何将LOTOS规范转换为C、C 语言实现进行了探讨。  相似文献   

4.
王继曾  张键 《微机发展》2004,14(2):78-81
形式描述技术在协议设计中的应用是至关重要的和必不可少的,为形式规范确定一个合适的结构又是应用此技术的关键步骤,基于此文中重点研究了基于LOTOS技术的形式结构模型的创建方法。简要介绍了开发网络协议的形式描述技术、网络协议的结构概念、等级抽象和LOTOS描述规范风格。基于LOTOS技术,提出了网络协议开发过程中形式结构模型的创建原则和方法,此方法结合LOTOS语言特征,应用其描述规范风格,融协议结构、逐步改进和等级抽象为一体,简化了所开发协议的验证、测试和实现的复杂性。  相似文献   

5.
本文介绍ISO最新开发的一种形式描述技术——LOTOS语言,这种语言以数学方法描述进程外观行为的时态次序,它定义了以事件为运算对象对行为表达式进行运算的一整套规则和相应的形式证明规则,从而为协议的正确说明与验证打下了基础。本文介紹事件和进程的描述方法,以及行为表达式的证明方法。读者可以发现,LOTOS有更广泛的应用。  相似文献   

6.
通信协议形式化模型的研究   总被引:5,自引:0,他引:5  
李腊元 《计算机学报》1998,21(5):419-427
本文提出了适应于通信协议的一类抽象形式化模型:抽象行为模型和抽象结构模型.前者主要包括事件、输入/输出、内部/外部和状态等子模型;后者主要包括交互点和分层子模型.文中讨论了这类形式模型的有效性和适用性,运用该类模型对通信协议的主要概念及性质进行了形式定义和描述.重点给出了基于该类模型的协议安全性及活性的形式定义,研讨了安全性及活性的验证,以及某些典型形式描述技术FDT(Estelle,LOTOS,SDL)之间的语义联系,从而为通信协议的研究提供了一种有效的形式基础.  相似文献   

7.
ISO/OSI会话层标准的形式化描述和开发   总被引:1,自引:0,他引:1  
本文通过对形式化描述技术LOTOS语言和ISO/OSI会话层标准的简要介绍,较详细地讨论了用LOTOS语言对OSI会话层的形式化规范描述,给出了其结构模型及一些重要的模块结构描述。  相似文献   

8.
为了实现由BPEL描述的Web服务组合到LOTOS的自动化转换, 提出一种基于翻译模式的转换算法。从BPEL语言的XML schema定义出发, 分析BPEL本身的语言结构, 得到BPEL语言的产生式。再根据BPEL到LOTOS的语义映射规则, 设计BPEL到LOTOS的翻译模式。同时, 在基本映射规则之上, 给出BPEL到LOTOS的数据类型和故障处理机制的转换规则。最后结合Web服务实例, 验证该工具的可行性。  相似文献   

9.
基于RSL的协议形式化描述与验证方法   总被引:2,自引:1,他引:1       下载免费PDF全文
讨论使用RAISE规范语言(RSL)描述6种协议元素的方法。在RSL描述的基础上,借助操作符的运算规则、并行扩展规则和同步会合事件隐藏规则,对协议的相关性质进行验证,以一个简化的停止等待协议规范的描述和验证实例证明,与其他形式化方法相比,RSL表现出较强的描述能力。  相似文献   

10.
谢冰  陈火旺  王兵山 《软件学报》1999,10(6):642-646
基于LOTOS规范语言,文章从系统功能规范出发,结合实际系统的分布特性,推导出符合实际系统结构的模块化规范的转换方法.用标注的完全LOTOS语言规范表达复杂的系统分布特性,研究了使用广播通信方式进行协同的、直接处理多模块划分的规范分解算法.  相似文献   

11.
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.
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,对分布环境下多媒体信息同步问题在实际中的应用,并与传统  相似文献   

16.
祝义  黄志球  曹子宁  周航  刘亚萍 《软件学报》2010,21(11):2738-2751
使用LOTOS描述实时系统需求规约,通过建立LOTOS规约到UML-RT模型的模型转换,提出一种基于形式化规约生成软件体系结构模型的方法。最后,通过一个实例来说明如何将该方法应用于实时软件建模。利用这种方法建立的UML-RT模型,能够从整体上提高实时系统软件体系结构设计的可信性。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号