网络协议设计中形式结构模型的创建方法研究

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

网络协议设计中形式结构模型的创建方法研究

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

MDA中从PIM到PSM的模型转换

基于在MDA中PIM到PSM的模型转换实现，提出了用UML描述PIM的一种有效性补充(E-)LOTOS，试图达到在模型映射前实现对模型的有效逻辑验证；对模型转换的基础理论进行了探索，分析了目前在MDA中实现从PIM到PSM模型转换的主要途径和困难；最后展望了模型转换的实现前景。     

映射ELOTOS到基于FSM的性能估价模型

ELOTOS是协议描述规范语言LOTOS的扩展．本文用标号转换系统LTS（labeledtransitionsystem）给出了ELOTOS的语义．然后，通过对LTS进行踪迹等价住分析，将ELOTOS映射到基于有穷状态机FSM（finitestatemachine）的性能估价模型．     

ISO／OSI会话层标准的形式化描述和开发

本文通过对形式化描述技术LOTOS语言和ISO/OSI会话层标准的简要介绍,较详细地讨论了用LOTOS语言对OSI会话层的形式化规范描述,给出了其结构模型及一些重要的模块结构描述。     

基于翻译模式的BPEL到LOTOS映射方法研究

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

测试目的引导的模型检测方法与技术研究

为了实现对伪代码的模型检测并且能够缓解模型检测中的状态空间爆炸问题,提出了测试目的引导的模型检测方法。该方法的基本思想是首先对伪代码进行模块划分并对每个模块进行建模,获取基本路径的集合并以流图的方式进行存储。然后利用自主开发的转换工具实现流图到国际标准语言LOTOS的转换。其次利用自主开发的辅助工具μ-演算编辑器对测试目的进行描述。最后使用模型检测工具验证被测程序是否满足测试目的。实验结果表明,测试目的引导的模型检测方法能够实现对伪代码的模型检测并且可以缓解状态空间爆炸问题。     

分布实现完全LOTOS规范的转换方法

基于LOTOS规范语言,文章从系统功能规范出发,结合实际系统的分布特性,推导出符合实际系统结构的模块化规范的转换方法.用标注的完全LOTOS语言规范表达复杂的系统分布特性,研究了使用广播通信方式进行协同的、直接处理多模块划分的规范分解算法.     

一种基于形式化规约生成软件体系结构模型的方法

使用LOTOS描述实时系统需求规约,通过建立LOTOS规约到UML-RT模型的模型转换,提出一种基于形式化规约生成软件体系结构模型的方法。最后,通过一个实例来说明如何将该方法应用于实时软件建模。利用这种方法建立的UML-RT模型,能够从整体上提高实时系统软件体系结构设计的可信性。     

协议形式化开发环境的规范语言

LOTOS（languageoftemporalorderingspecification）是一种基于进程代数CCS的协议规范语言，面向协议验证，但它不能描述协议的某些性质．本文提出了一种LOTOS的扩充语言ELOTOS（extendedLOTOS），它在LOTOS的基础上引入了异步通讯机制、时间描述、事件发生的随机性描述．     

Rapid prototyping of protocols from LOTOS specifications

A new tool for generating implementation prototypes of communication protocols and concurrent systems specified using the ISO LOTOS language is presented in this paper. A brief introduction to LOTOS and a discussion of the main problems related to the efficient execution of specifications written in LOTOS are presented first. The design and implementation of the tool are then considered: LOTOS specifications are analysed and translated into C functions which are executed by co-operating processes in the Unix environment. The set of LOTOS process definitions is first translated into a suitable number of extended finite-state machines (EFSMs). The method proposed allows the problem of deriving unbounded EFSMs to be circumvented and a sort of control on the process number/size trade-off to be obtained at the same time. The problem of implementing the LOTOS multi-way rendezvous mechanism for process synchronization is solved by using an algorithm based on message-passing techniques. An example of prototype derivation is also described, showing the form of C code generated by translating a simple specification. Finally, some performance figures are presented.     

An interpreter for LOTOS,a specification language for distributed systems

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.     

Use of a formal description technique in the specification of authentication protocols

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.     

Development of an atomic‐broadcast protocol using LOTOS

In this article we report on the development of a group‐communication service using the formal specification language LOTOS, and present our experience in using publicly available tools for this purpose. The service implements atomic broadcast through a Two‐Phase‐Commit protocol, providing at‐least‐once delivery semantics and with no restriction on message delivery order. First we wrote an informal specification describing the desired properties from the service, the interfaces with the underlying network layer and the upper user layer, and the protocol to be used by the service. Then we developed the formal specification of the protocol in LOTOS. After validating the formal specification and thus having a certain confidence in its adequacy with respect to the informal specification, we derived test cases from the formal specification and implemented the service using the Concert/C distributed programming language. While testing the implementation, we found that most errors were related to unspecified features or bugs in the execution environment. From this experience, we draw our conclusions on the usefulness of software development based on formal techniques. Copyright © 1999 John Wiley & Sons, Ltd.     

Incremental requirements specification withLotos

The importance of formally and incrementally specifying requirements is discussed. An approach based on LOTOS (Language Of Temporal Ordering Specification) is proposed that exploits desirable characteristics of the constraint-oriented style. The nature of constraint-oriented specification is discussed at some length, and guidelines for how to use it effectively with LOTOS are presented. Small introductory examples lead to the incremental specification of a file access system using the approach in the paper. It is shown how the requirements for the file access system can be gradually formalised, leading to a complete system specification.     

On the formal specification and verification of CIM architectures using LOTOS

A computer Integrated Manufacturing (CIM) architecture is a specification that prescribes, in an implementation-independent way, how parts of a CIM system must cooperate by exchanging messages and products. Good architectures prevent costly redesign of already installed CIM system parts that cannot cooperate.To ensure that CIM architectures leave no room for ambiguous interpretation, they should be defined in a formal language. Some requirements for a formal specification language for CIM architectures are discussed. It is shown that the language LOTOS, developed by the International Organisation for Standardization, is suitable for this purpose.A sample CIM architecture is specified using LOTOS. It is an architecture of a ‘workcell’ comprising ‘workstations’, a ‘workcell controller’ and a ‘transport system’. LOTOS transformation laws are applied to prove that this workcell delivers completed products, which is not evident at first sight.